created by

Vincent Aravantinos

script type

syntax

description

All is in the title: syntax colouring for the coq proof assistant files (*.v). Also check http://www.vim.org/scripts/script.php?script_id=2079 for indentation. Some people asked me if I planned to do something to interact between vim and coq. I answered that yes and that I had started it. The plugin is usable but not “publishable" :) However I now have many other things to do and am not using Coq at that time. So if I publish such a thing some day it may be in quite a long time. Apologies.

install details

1. Put the file in your ~/.vim/syntax directory. 2. Create the file ~/.vim/ftdetect/coq.vim and put the following line inside:   au BufRead,BufNewFile *.v   set filetype=coq (Notice that *.v files are also used for verilog sources. This will make vim recognize *.v files as coq ones. VERILOG FILES WON'T BE RECOGNIZED ANYMORE.)

Click on the package to download.

package	script version	date	Vim version	user	release notes
coq.vim	1.4.3	2008-12-02	6.0	Vincent Aravantinos	Added Program and Obligations constructs of Coq v8.2.
coq.vim	1.4	2008-01-27	7.0	Vincent Aravantinos	- Changed the colours. It should now be more uniform and more readable. Tell me if you prefer the way it was before. - Improved the way things are coloured : in previous versions, the plugin often had to wait until you finish the current sentence before colouring it. Quite inconvenient. Now, it will colour things as you type them (for almost all constructions). Colouring is also more robust.
coq.vim	1.0	2007-11-07	7.0	Vincent Aravantinos	Complete refactoring. Highlighting is now much more accurate. Oh, and the code is not ugly anymore.
coq.vim	0.01	2007-11-06	7.0	Vincent Aravantinos	Initial upload

ip used for rating: 18.226.177.223