医者に行った

半年くらい前から、少し歌うとすぐに喉が枯れるようになった。

それで、喉が痛いと言って医者にかかったはずが、なぜか胃カメラを飲んでいた。
（逆流性食道炎の可能性ありとかなんとか）
しかし喉も食道も胃も綺麗なもんだそうだ。
相変わらず喉は痛い。

今日のCoq

CoqはProofGeneralで最後まで解釈出来るのに、coqcコマンドでエラーが起きる。

$ coqc List_J.v
Warning: Not interpreting "*)" as the end of current non-terminated comment because it occurs in a non-terminated string of the comment.
Warning: Not interpreting "*)" as the end of current non-terminated comment because it occurs in a non-terminated string of the comment.


途中省略


because it occurs in a non-terminated string of the comment.
Warning: Not interpreting "*)" as the end of current non-terminated comment because it occurs in a non-terminated string of the comment.
File "./List_J.v", line 874, characters 17-2108:
Syntax error: Unterminated string.

874行目前後の記述は

  simpl. reflexivity.
  SCase "m = S m'". 
  simpl.  apply IHn'.

のようになんの変哲もない。
問題はコメントなのか？文字列なのか？それすらわからん。

原因解明

coqc -verbose List_J.v
でどこまで構文解析したか出た。
コメント中に、 "( という記述があると不味いようだ。そんなん知るかーー
" や、（ 単独だと問題なさげ。
coqcのバージョンがちと古いのかな。

# coqc -v
The Coq Proof Assistant, version 8.3pl4 (June 2012)
compiled on Jun 08 2012 17:28:01 with OCaml 3.12.1