Hi all !
for a long time, the Coq project has been using the OCaml feature that allows to use “interface-only” modules, that is to say, modules defined by a single
mli file which don’t provide the corresponding
However, we are aware of some limitations wrt to modules without an implementation, such as
https://caml.inria.fr/mantis/view.php?id=6923 , and we have heard of some other issues as for instance with packing.
So the the Coq developers have been wondering for a while if we should migrate away from the
.mli only setup? Are there plans in OCaml to support
.mli-only modules as first class citizens in the future?
Thanks for any help! Cheers, E.
edit: Link to Coq’s “intf” files: https://github.com/coq/coq/tree/v8.6/intf