diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-24 17:30:06 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-24 17:30:06 +0000 |
| commit | 3396e2d3a3abe0a740302a6e87b529a1ebcbc08e (patch) | |
| tree | c68aa163635d586fd9d34d19e29cbae51a72a65e /library/nametab.mli | |
| parent | 4fd6bfd7204a2371f7b8f5c3a34fb2feaa273193 (diff) | |
Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametab
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@947 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/nametab.mli')
| -rwxr-xr-x | library/nametab.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/library/nametab.mli b/library/nametab.mli index 9a90a70b8..54c4bc67b 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -29,6 +29,7 @@ val locate_obj : qualid -> (section_path * Libobject.obj) val locate_constant : qualid -> constant_path val open_module_contents : string -> unit +val rec_open_module_contents : string -> unit |