Nettoyage

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

4 files changed, 19 insertions, 7 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 7c642a1fd..8aa6949e3 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -354,8 +354,12 @@ let constr_of_reference sigma env ref =
   in
   find_common_hyps_then_abstract body env0 hyps0 hyps
 
-let construct_qualified_reference env sp =
-  let ref = Nametab.locate sp in
+let construct_absolute_reference env sp =
+  let ref = Nametab.locate (qualid_of_sp sp) in
+  constr_of_reference Evd.empty env ref
+
+let construct_qualified_reference env qid =
+  let ref = Nametab.locate qid in
   constr_of_reference Evd.empty env ref
 
 let construct_reference env kind id =
@@ -365,8 +369,11 @@ let construct_reference env kind id =
   with Not_found ->
     mkVar (let _ = Environ.lookup_named id env in id)
 
-let global_qualified_reference sp = 
-  construct_qualified_reference (Global.env()) sp
+let global_qualified_reference qid = 
+  construct_qualified_reference (Global.env()) qid
+
+let global_absolute_reference sp = 
+  construct_absolute_reference (Global.env()) sp
 
 let global_reference kind id = 
   construct_reference (Global.env()) kind id
@@ -385,7 +392,7 @@ let dirpath_of_global = function
 
 let is_global id =
   try 
-    let osp = Nametab.sp_of_id CCI id in
+    let osp = Nametab.locate (make_qualid [] id) in
     list_prefix_of (dirpath_of_global osp) (Lib.cwd())
   with Not_found -> 
     false
diff --git a/library/declare.mli b/library/declare.mli
index 01ecc484a..78f19e68f 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -75,9 +75,13 @@ val constr_of_reference :
   'a Evd.evar_map -> Environ.env -> global_reference -> constr
 
 val global_qualified_reference : qualid -> constr
-val global_reference : path_kind -> identifier -> constr
+val global_absolute_reference : section_path -> constr
 
 val construct_qualified_reference : Environ.env -> qualid -> constr
+val construct_absolute_reference : Environ.env -> section_path -> constr
+
+(* This should eventually disappear *)
+val global_reference : path_kind -> identifier -> constr
 val construct_reference : Environ.env -> path_kind -> identifier -> constr
 
 val is_global : identifier -> bool
diff --git a/library/nametab.ml b/library/nametab.ml
index 595f3b58a..b116dda20 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -146,7 +146,7 @@ let _ =
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
       Summary.init_function = init;
-      Summary.survive_section = true }
+      Summary.survive_section = false }
 
 let rollback f x =
   let fs = freeze () in
diff --git a/library/nametab.mli b/library/nametab.mli
index 1d39eb310..cb09d39a8 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -19,6 +19,7 @@ val push : section_path -> global_reference -> unit
 val push_object : section_path -> Libobject.obj -> unit
 val push_module : section_path -> module_contents -> unit
 
+(* This should eventually disappear *)
 val sp_of_id : path_kind -> identifier -> global_reference
 
 (* This returns the section path of a constant or fails with [Not_found] *)