Coq 8.16.0 では、以前報告した、 Coq Issue #7061: OCaml extraction can generate infinite recursion という問題が直っているようだ
これで、たぶん、(再度) strong normalization になったと思うのだが...
[latest]