sponsor Vim development Vim logo Vim Book Ad

coq syntax : syntax colouring for coq files

 script karma  Rating 34/18, Downloaded by 1981    Comments, bugs, improvements  Vim wiki

created by
Vincent Aravantinos
script type
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.)

rate this script Life Changing Helpful Unfulfilling 
script versions (upload new version)

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:

If you have questions or remarks about this site, visit the vimonline development pages. Please use this site responsibly.
Questions about Vim should go to the maillist. Help Bram help Uganda.
SourceForge.net Logo