find_section_variable : un traducteur id -> sp pour variables de section; variable_strength change de type

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

2 files changed, 17 insertions, 8 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 4d76ef8aa..621666d67 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -236,10 +236,8 @@ let get_variable sp =
   let (c,ty) = Global.lookup_named id in
   ((id,c,ty),str,sticky)
 
-let variable_strength qid =
-  match Nametab.locate qid with
-    | VarRef sp -> let _,(_,str,_) = Spmap.find sp !vartab in str
-    | _ -> anomaly "variable_strength: not the reference to a variable"
+let variable_strength sp =
+  let _,(_,str,_) = Spmap.find sp !vartab in str
 
 (* Global references. *)
 
@@ -326,6 +324,16 @@ let current_section_context () =
     (fun (id,_,_ as d) hyps -> if List.mem id current then d::hyps else hyps)
     (Global.named_context ()) []
 
+let find_section_variable id =
+  let l =
+    Spmap.fold
+      (fun sp (id',_) hyps -> if id=id' then sp::hyps else hyps)
+      !vartab [] in
+  match l with
+    | [] -> raise Not_found
+    | [sp] -> sp
+    | _ -> error "Arghh, you blasted me with several variables of same name"
+
 let extract_instance ref args =
   let hyps = context_of_global_reference Evd.empty (Global.env ()) ref in
   let hyps0 = current_section_context () in
diff --git a/library/declare.mli b/library/declare.mli
index 5f9f8ba36..3c5e99608 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -56,12 +56,13 @@ val make_strength_2 : unit -> strength
 (*s Corresponding test and access functions. *)
 
 val is_constant : section_path -> bool
-val constant_strength : section_path -> strength
-val constant_or_parameter_strength : section_path -> strength
+val constant_strength : constant_path -> strength
+val constant_or_parameter_strength : constant_path -> strength
 
 val out_variable : Libobject.obj -> identifier * variable_declaration
-val get_variable : section_path -> named_declaration * strength * sticky
-val variable_strength : qualid -> strength
+val get_variable : variable_path -> named_declaration * strength * sticky
+val variable_strength : variable_path -> strength
+val find_section_variable : identifier -> section_path
 
 (*s [global_reference k id] returns the object corresponding to
     the name [id] in the global environment. It may be a constant,