Removing some generic equalities.

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

5 files changed, 11 insertions, 7 deletions

diff --git a/kernel/context.ml b/kernel/context.ml
index 930ab75081..bdc4c067a6 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -90,7 +90,8 @@ let rec lookup_named id = function
 let named_context_length = List.length
 let named_context_equal = List.equal eq_named_declaration
 
-let vars_of_named_context = List.map (fun (id,_,_) -> id)
+let vars_of_named_context ctx =
+  List.fold_left (fun accu (id, _, _) -> Id.Set.add id accu) Id.Set.empty ctx
 
 let instance_from_named_context sign =
   let filter = function
diff --git a/kernel/context.mli b/kernel/context.mli
index ad6d645cd3..048edef951 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -56,7 +56,7 @@ type rel_context = rel_declaration list
 
 val empty_named_context : named_context
 val add_named_decl : named_declaration -> named_context -> named_context
-val vars_of_named_context : named_context -> Id.t list
+val vars_of_named_context : named_context -> Id.Set.t
 
 val lookup_named : Id.t -> named_context -> named_declaration
 
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 0a96821a33..65efb4fd0d 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -18,6 +18,9 @@ open Names
  *)
 type level = Expand | Level of int | Opaque
 let default = Level 0
+let is_default = function
+| Level 0 -> true
+| _ -> false
 let transparent = default
 let is_transparent = function
 | Level 0 -> true
@@ -45,11 +48,11 @@ let set_strategy k l =
   match k with
   | VarKey id ->
       var_opacity :=
-      if l=default then Id.Map.remove id !var_opacity
+      if is_default l then Id.Map.remove id !var_opacity
       else Id.Map.add id l !var_opacity
   | ConstKey c ->
       cst_opacity :=
-      if l=default then Cmap.remove c !cst_opacity
+      if is_default l then Cmap.remove c !cst_opacity
       else Cmap.add c l !cst_opacity
   | RelKey _ -> Errors.error "set_strategy: RelKey"
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 9b18db78e8..ae6817a76d 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -228,7 +228,7 @@ let lookup_constructor_variables (ind,_) env =
 
 let vars_of_global env constr =
   match kind_of_term constr with
-      Var id -> [id]
+      Var id -> Id.Set.singleton id
     | Const kn -> lookup_constant_variables kn env
     | Ind ind -> lookup_inductive_variables ind env
     | Construct cstr -> lookup_constructor_variables cstr env
@@ -239,7 +239,7 @@ let global_vars_set env constr =
     let acc =
       match kind_of_term c with
       | Var _ | Const _ | Ind _ | Construct _ ->
-	  List.fold_right Id.Set.add (vars_of_global env c) acc
+	  Id.Set.union (vars_of_global env c) acc
       | _ ->
 	  acc in
     fold_constr filtrec acc c
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 54e88f6464..d378501a0f 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -165,7 +165,7 @@ val set_engagement : engagement -> env -> env
 val global_vars_set : env -> constr -> Id.Set.t
 
 (** the constr must be a global reference *)
-val vars_of_global : env -> constr -> Id.t list
+val vars_of_global : env -> constr -> Id.Set.t
 
 val keep_hyps : env -> Id.Set.t -> section_context