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

3 files changed, 24 insertions, 2 deletions

diff --git a/library/declare.ml b/library/declare.ml
index e6d6247a0..fc6a6d10b 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -367,8 +367,7 @@ let constr_of_reference sigma env ref =
   find_common_hyps_then_abstract body env0 hyps0 hyps
 
 let construct_absolute_reference env sp =
-  let ref = Nametab.locate (qualid_of_sp sp) in
-  constr_of_reference Evd.empty env ref
+  constr_of_reference Evd.empty env (Nametab.absolute_reference sp)
 
 let construct_qualified_reference env qid =
   let ref = Nametab.locate qid in
diff --git a/library/nametab.ml b/library/nametab.ml
index 57002455b..595f699a4 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -83,6 +83,11 @@ let push_module sp mc =
     warning ("Cannot allow access to "^s^" by relative paths: it is already registered as a root of the Coq library")
   else push_mod_current s (sp,mc)
 
+(* Sections are not accessible by basename *)
+let push_section sp mc =
+  let dir, s = repr_qualid (qualid_of_sp sp) in
+  push_mod_absolute dir s (sp,mc)
+
 (* This is an entry point for local declarations at toplevel *)
 (* Do not use with "open" since it pushes an absolute name too *)
 
@@ -143,6 +148,14 @@ let constant_sp_of_id id =
     | ConstRef sp -> sp
     | _ -> raise Not_found
 
+let check_absoluteness = function
+  | a::_ when List.mem a !roots -> ()
+  | _ -> anomaly "Not an absolute path"
+
+let absolute_reference sp =
+  check_absoluteness (dirpath sp);
+  locate (qualid_of_sp sp)
+
 (* These are entry points to make the contents of a module/section visible *)
 (* in the current env (does not affect the absolute name space `coq_root') *)
 let open_module_contents qid =
@@ -151,6 +164,8 @@ let open_module_contents qid =
 (*  Stringmap.iter (fun _ -> Libobject.open_object) objtab;*)
   Stringmap.iter push_mod_current modtab
 
+let open_section_contents = open_module_contents
+
 let rec rec_open_module_contents qid =
   let _, (Closed (ccitab,objtab,modtab)) = locate_module qid in
   Stringmap.iter push_cci_current ccitab;
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