Coq で extract したコードを ocamlopt で native code にコンパイルしたら、tail call optimization が効かなくて悲しい。
coq-bugs 4312: ocamlopt can not optimize tail call in a extracted function.
OCaml と Coq のどちらの問題か迷うところだが、Coq のほうに報告してみた。
[latest]