Known to be compatible with OCaml 4 and 5, Coq 8.14 to 8.20, HOL4 trindemossen-1.
- 2023-12 @MSoegtropIMC: Windows opam build fix
- 2024-04 @palmskog: Coq 8.19 compatibility
- 2024-09 @palmskog: output simplified HOL4 Inductive syntax for trindemossen-1 and later, modernise HOL4 libraries
- 2024-11 @bacam: fix marshalling
- 2024-12 @palmskog: add explicit locality to generated Coq Hint commands
- 2024-12 @palmskog: move y2l to non-aux directory to avoid Windows problems, fix doc build
- 2024-12 @palmskog: add coq-notation hom to allow using Coq Notation sentences instead of Definition
- 2024-12 @palmskog: only output plain comments in generated Coq code
Contributors
palmskog, bacam, and MSoegtropIMC