Coqのソースコードをocamldebugで追えるようにして早何日か。 結局ocamldebugを使うのは（少なくとも現時点では）諦めることにした。 理由は次の通り。 Coqが使っている構文解析器がそもそもocamlcでコンパイルするものじゃなかった*1。 多相がものすごく邪…

研究の関係上、とあるOCamlのプロジェクト――いえ、まあ、とあるもなにも、Coqだが――をいじる必要が出た。 そんなにプログラミング・・・というかプロジェクトの読み解きなどをやったことがない私は、途方にくれ・・・まではしなかった。 運がいいことに、先…