Non-termination

Gitlab

• Some recursive functions in the imported OCaml code do not terminate for Coq because of the guard condition. This condition is disabled for functions that do not terminate for Coq.
• simpl may fail if the {struct} parameter is not the right one. To safely unfold an iteration step, you can use cbv delta [function_name] or the Arguments command https://coq.inria.fr/refman/language/extensions/arguments-command.html#effects-of-arguments-on-unfolding