Meilleur traitement des noms explicites dans la Nametab; Différentation du traitement des sections et des modules

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1328 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 0 deletions

diff --git a/library/nametab.mli b/library/nametab.mli
index 7f43b9d84..64cba70c2 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -40,6 +40,10 @@ val exists_module : section_path -> bool
 val open_module_contents : qualid -> unit
 val rec_open_module_contents : qualid -> unit
 
+(*s Entry points for sections *)
+val open_section_contents : qualid -> unit
+val push_section : section_path -> module_contents -> unit
+
 (*s Roots of the space of absolute names *)
 
 (* This is the root of the standard library of Coq *)
@@ -51,3 +55,7 @@ val default_root : string
 (* This is to declare a new root *)
 val push_library_root : string -> unit
 
+(* This turns a "user" absolute name into a global reference;
+   especially, constructor/inductive names are turned into internal
+   references inside a block of mutual inductive *)
+val absolute_reference : section_path -> global_reference