---

Ⅰ. 插件描述

A simple Vim plugin for the Coq Proof Assistant

Ⅱ. 基本信息

创建日期：  2014-12-01 使用用户：  6 Github星：  4 插件作者：  TOUNAI Shouta

Ⅲ. 安装方法

使用Vundle管理器安装

在你的.vimrc下添加:

Plugin 'tounaishouta/coq-vim-red'

… 然后在Vim中运行以下命令:

:source %
:PluginInstall

对于Vundle版本 < 0.10.2，请用上面的Bundle替换Plugin。

使用NeoBundle管理器安装

在你的.vimrc下添加:

NeoBundle 'tounaishouta/coq-vim-red'

… 然后在Vim中运行以下命令:

:source %
:NeoBundleInstall

使用VimPlug管理器安装

在你的.vimrc下添加:

Plug 'tounaishouta/coq-vim-red'

… 然后在Vim中运行以下命令:

:source %
:PlugInstall

使用Pathogen管理器安装

在终端中运行以下命令:

cd ~/.vim/bundle
git clone https://github.com/tounaishouta/coq.vim

Ⅳ. 文档说明

coq.vim

Overview

A simple Vim plugin for the Coq Proof Assistant.

Description

When editing a Coq file (filename: *.v) whithin Vim,
this plugin provides the function of "Go to cursor" command of CoqIde,
that is,
run coqtop command with lines to cursor, and
display the output in a new split window.

Usage

This function is provided as Ex command:

:CoqRunToCursor

I recommend to write a key bind in .vimrc, like:

autocmd Filetype coq nnoremap ,, :CoqRunToCursor<CR>

Install

Write in .vimrc

NeoBundle 'tounaishouta/coq.vim'

or place this plugin somewhere and write in .vimrc

set runtimepath+=path/to/this/plugin/coq.vim

License

This plugin is placed in the public domain.
The indent files is a copy of http://www.vim.org/scripts/script.php?script_id=2079 .
The syntax files is a copy of http://www.vim.org/scripts/script.php?script_id=2063 .

Author

TOUNAI Shouta [tounai.shouta@gmail.com]

History

2014 Dec 15: write README.md
2014 Dec 16: copied indent and syntax files from vim-scripts
2015 Mar 02: change user name