Open
Milestone
Translate in Coq 馃悡
The goal of this milestone is to have a version of the library compiling in Coq, after a translation using coq-of-ocaml
. The Coq translation may not necessarily be complete. For example, the side-effects (exceptions, references) may be axiomatized.