*** empty log message ***

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

6 files changed, 31 insertions, 16 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 2b452ecbb6..aa2c6c1db9 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -255,7 +255,7 @@ let inductive_class_of ind = fst (class_info (CL_IND ind))
 let class_args_of c = snd (decompose_app c)
 
 let strength_of_cl = function 
-  | CL_CONST kn -> constant_strength (sp_of_global None (ConstRef kn))
+  | CL_CONST kn -> constant_strength (sp_of_global (ConstRef kn))
   | CL_SECVAR sp -> variable_strength sp
   | _ -> Global
 
@@ -263,11 +263,11 @@ let string_of_class = function
   | CL_FUN -> "FUNCLASS"
   | CL_SORT -> "SORTCLASS" 
   | CL_CONST sp ->
-      string_of_qualid (shortest_qualid_of_global None (ConstRef sp))
+      string_of_qualid (shortest_qualid_of_global Idset.empty (ConstRef sp))
   | CL_IND sp ->
-      string_of_qualid (shortest_qualid_of_global None (IndRef sp))
+      string_of_qualid (shortest_qualid_of_global Idset.empty (IndRef sp))
   | CL_SECVAR sp ->
-      string_of_qualid (shortest_qualid_of_global None (VarRef sp))
+      string_of_qualid (shortest_qualid_of_global Idset.empty (VarRef sp))
 
 (* coercion_value : coe_index -> unsafe_judgment * bool *)
 
@@ -393,7 +393,7 @@ let coercion_of_qualid qid =
   let coe = coe_of_reference ref in
   if not (coercion_exists coe) then
     errorlabstrm "try_add_coercion" 
-      (Nametab.pr_global_env None ref ++ str" is not a coercion");
+      (Nametab.pr_global_env Idset.empty ref ++ str" is not a coercion");
   coe
 
 module CoercionPrinting =
@@ -401,7 +401,7 @@ module CoercionPrinting =
     type t = coe_typ
     let encode = coercion_of_qualid
     let subst = subst_coe_typ
-    let printer x = pr_global_env None x
+    let printer x = pr_global_env Idset.empty x
     let key = Goptions.SecondaryTable ("Printing","Coercion")
     let title = "Explicitly printed coercions: "
     let member_message x b =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index f0f07e06e4..f676717d71 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -70,7 +70,7 @@ module PrintingCasesMake =
       let kn' = subst_kn subst kn in
 	if kn' == kn then obj else
 	  (kn',i), ints
-    let printer (ind,_) = pr_global_env None (IndRef ind)
+    let printer (ind,_) = pr_global_env Idset.empty (IndRef ind)
     let key = Goptions.SecondaryTable ("Printing",Test.field)
     let title = Test.title
     let member_message x = Test.member_message (printer x)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index ed549a77ed..1b7a515b93 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -560,7 +560,7 @@ let lookup_eliminator ind_sp s =
   (* inductive type *)
   let ref = ConstRef (make_kn mp dp (label_of_id id)) in
   try 
-    let _ = sp_of_global None ref in
+    let _ = sp_of_global ref in
       constr_of_reference ref
   with Not_found ->
   (* Then try to get a user-defined eliminator in some other places *)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 7613cd6df7..2a74ede726 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -33,7 +33,7 @@ let set_transparent_const sp =
   if cb.const_body <> None & cb.const_opaque then
     errorlabstrm "set_transparent_const"
       (str "Cannot make" ++ spc () ++ 
-         Nametab.pr_global_env None (ConstRef sp) ++
+         Nametab.pr_global_env Idset.empty (ConstRef sp) ++
          spc () ++ str "transparent because it was declared opaque.");
   Conv_oracle.set_transparent_const sp
 
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index b233ce2441..a41631bd2b 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -537,7 +537,19 @@ let first_char id =
 
 let lowercase_first_char id = String.lowercase (first_char id)
 
-let id_of_global env ref = Nametab.id_of_global (Some (named_context env)) ref
+let vars_of_env env =
+  let s = 
+    Sign.fold_named_context (fun (id,_,_) s -> Idset.add id s)
+      (named_context env) ~init:Idset.empty in
+  Sign.fold_rel_context
+    (fun (na,_,_) s -> match na with Name id -> Idset.add id s | _ -> s)
+    (rel_context env) ~init:s
+
+let add_vname vars = function
+    Name id -> Idset.add id vars
+  | _ -> vars
+
+let id_of_global = Nametab.id_of_global
 
 let sort_hdchar = function
   | Prop(_) -> "P"
@@ -558,9 +570,9 @@ let hdchar env c =
 	if i=0 then 
 	  lowercase_first_char (id_of_label (label kn))
 	else 
-	  lowercase_first_char (id_of_global env (IndRef x))
+	  lowercase_first_char (id_of_global (IndRef x))
     | Construct ((sp,i) as x) ->
-	lowercase_first_char (id_of_global env (ConstructRef x))
+	lowercase_first_char (id_of_global (ConstructRef x))
     | Var id  -> lowercase_first_char id
     | Sort s -> sort_hdchar s
     | Rel n ->
@@ -671,12 +683,12 @@ let occur_rel p env id =
 let occur_id env nenv id0 c =
   let rec occur n c = match kind_of_term c with
     | Var id when  id=id0 -> raise Occur
-    | Const kn when id_of_global env (ConstRef kn) = id0 -> raise Occur
+    | Const kn when id_of_global (ConstRef kn) = id0 -> raise Occur
     | Ind ind_sp
-	when id_of_global env (IndRef ind_sp) = id0 ->
+	when id_of_global (IndRef ind_sp) = id0 ->
         raise Occur
     | Construct cstr_sp
-	when id_of_global env (ConstructRef cstr_sp) = id0 ->
+	when id_of_global (ConstructRef cstr_sp) = id0 ->
         raise Occur
     | Rel p when p>n & occur_rel (p-n) nenv id0 -> raise Occur
     | _ -> iter_constr_with_binders succ occur n c
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 0cd757ceda..cd5d7def0f 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -114,7 +114,6 @@ val eta_eq_constr : constr -> constr -> bool
 (* finding "intuitive" names to hypotheses *)
 val first_char : identifier -> string
 val lowercase_first_char : identifier -> string
-(*val id_of_global : env -> Libnames.global_reference -> identifier*)
 val sort_hdchar : sorts -> string
 val hdchar : env -> types -> string
 val id_of_name_using_hdchar :
@@ -144,6 +143,10 @@ val ids_of_named_context : named_context -> identifier list
 val ids_of_context : env -> identifier list
 val names_of_rel_context : env -> names_context
 
+(* Set of local names *)
+val vars_of_env: env -> Idset.t
+val add_vname : Idset.t -> name -> Idset.t
+
 (* sets of free identifiers *)
 type used_idents = identifier list
 val occur_rel : int -> name list -> identifier -> bool