search

the-lambda-church / coquille

Interactive theorem proving with Coq in vim.
ISC License
186 stars 68 forks source link

provide details on pathogen installation #41

Open dimpase opened 8 years ago

dimpase commented 8 years ago

the minimal pathogen setup 

execute pathogen#infect()
syntax on
filetype plugin indent on

does not work with coquille; specifically, :CoqLaunch does not work (vim 7.4.52 on Ubuntu 14.04). What it should expand to, i.e. :call coquille#Launch(), does do something, but any attempt to type in the interaction window results in:

 Error detected while processing InsertEnter Auto commands for "<buffer=1>":
 Traceback (most recent call last):
renovatorruler commented 7 years ago

Same problem here