http://www.iij-ii.co.jp/lab/techdoc/coqt/ を読んでいたらいつのまにかそんなかんじのを書いていた.どうしても Vim で書きたいかわいそうな人以外は普通に CoqIDE や Proof General 使ったほうがいいと思います. https://github.com/eagletmt/coqtop-vim 最新の vimproc を先にインストールしておく必要がある. 使い方としてはまず :CoqStart で coqtop からの出力を表示するバッファとウィンドウを作る. コードを書いていき,インサートモードで するとその行まで coqtop に送られる.ノーマルモードで :CoqGoto あるいは g *1でも同じ. 既に送られた領域の最後の行は Folded で色付けされ,これより上の行は編集できなくなる. (ところで「編集できなく」するため