+Yoshihiro Imai さんの Coq for beginners  http://www.slideshare.net/yoshihiro503/coq-for-beginners を読んで、Coqのコマンド言語にVernacularという名前があったことを知った。。。