diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-06 22:39:43 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-06 22:39:43 +0000 |
| commit | a1fe45ddbd37d3c447a23cde0ee21f105ef42ac0 (patch) | |
| tree | 648a977d3137ffa9c7cc97e8503c0a5d8620dbfa /interp/modintern.mli | |
| parent | 0cdfa2fb137989f75cdebfa3a64726bc0d56a8af (diff) | |
Enhancements to coqdoc, better globalization of sections and modules.
Minor fix in Morphisms which prevented working with higher-order
morphisms and PER relations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11065 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/modintern.mli')
| -rw-r--r-- | interp/modintern.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/interp/modintern.mli b/interp/modintern.mli index 1f27e3c18..c14b6481e 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -26,3 +26,6 @@ val interp_modtype : env -> module_type_ast -> module_struct_entry val interp_modexpr : env -> module_ast -> module_struct_entry val lookup_module : qualid located -> module_path + +val dump_moddef : loc -> module_path -> string -> unit +val dump_modref : loc -> module_path -> string -> unit |