Skip to content

Integrating Coq proofs

Joe Nelson edited this page Jun 14, 2014 · 2 revisions

To enable support for checking Coq proof checking, add the following to your vimrc.local, then run :BundleUpdate.

" using Vundle for modules
Bundle 'def-lkb/vimbufsync'
Bundle 'the-lambda-church/coquille'

" configure key bindings and colors
augroup coqColors
 autocmd!
 autocmd BufReadPost *.v hi CheckedByCoq ctermbg=17 guibg=#111133
 autocmd BufReadPost *.v hi SentToCoq ctermbg=60 guibg=#222244
augroup END

map <silent> <leader>cs :CoqLaunch<cr>
map <silent> <leader>cg :CoqToCursor<cr>
map <silent> <leader>cn :CoqNext<cr>
map <silent> <leader>cu :CoqUndo<cr>
map <silent> <leader>cq :CoqKill<cr>

map <silent> <leader>cx <C-w>l<C-w>L<C-w>t<C-w>K
map <silent> <leader>cp :execute "Coq Print " . expand("<cword>") . "."<cr>