cList: set-as-list functions are now with an explicit comparison

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

7 files changed, 18 insertions, 10 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 72df29e25..c9f00c0cd 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -543,7 +543,9 @@ let rec find_dependency_list tmblock = function
   | (used,tdeps,d)::rest ->
       let deps = find_dependency_list tmblock rest in
       if used && List.exists (fun x -> dependent_decl x d) tmblock
-      then List.add_set (List.length rest + 1) (List.union deps tdeps)
+      then
+        List.add_set Int.equal
+          (List.length rest + 1) (List.union Int.equal deps tdeps)
       else deps
 
 let find_dependencies is_dep_or_cstr_in_rhs (tm,(_,tmtypleaves),d) nextlist =
@@ -688,7 +690,7 @@ let get_names env sign eqns =
   (* Otherwise, we take names from the parameters of the constructor but
      avoiding conflicts with user ids *)
   let allvars =
-    List.fold_left (fun l (_,_,eqn) -> List.union l eqn.rhs.avoid_ids)
+    List.fold_left (fun l (_,_,eqn) -> List.union Id.equal l eqn.rhs.avoid_ids)
       [] eqns in
   let names3,_ =
     List.fold_left2
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index d242dbc34..1cc9df024 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -681,7 +681,9 @@ let retract_coercible_metas evd =
 
 let subst_defined_metas bl c =
   let rec substrec c = match kind_of_term c with
-    | Meta i -> substrec (List.assoc_snd_in_triple i bl)
+    | Meta i ->
+      let select (j,_,_) = Int.equal i j in
+      substrec (pi2 (List.find select bl))
     | _ -> map_constr substrec c
   in try Some (substrec c) with Not_found -> None
 
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index e6a95a03e..329af8526 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -212,7 +212,7 @@ let instantiate_pattern sigma lvar c =
 	with Not_found (* List.index failed *) ->
 	  let vars =
 	    List.map_filter (function Name id -> Some id | _ -> None) vars in
-	  error_instantiate_pattern id (List.subtract ctx vars)
+	  error_instantiate_pattern id (List.subtract Id.equal ctx vars)
        with Not_found (* Map.find failed *) ->
 	 x)
   | (PFix _ | PCoFix _) -> error ("Non instantiable pattern.")
diff --git a/pretyping/redops.ml b/pretyping/redops.ml
index 1713a371e..687cf6e46 100644
--- a/pretyping/redops.ml
+++ b/pretyping/redops.ml
@@ -8,6 +8,8 @@
 
 open Genredexpr
 
+let union_consts l1 l2 = Util.List.union Pervasives.(=) l1 l2 (* FIXME *)
+
 let make_red_flag l =
   let rec add_flag red = function
     | [] -> red
@@ -18,14 +20,14 @@ let make_red_flag l =
 	if red.rDelta then
 	  Errors.error
 	    "Cannot set both constants to unfold and constants not to unfold";
-        add_flag { red with rConst = Util.List.union red.rConst l } lf
+        add_flag { red with rConst = union_consts red.rConst l } lf
     | FDeltaBut l :: lf ->
 	if red.rConst <> [] && not red.rDelta then
 	  Errors.error
 	    "Cannot set both constants to unfold and constants not to unfold";
         add_flag
-	  { red with rConst = Util.List.union red.rConst l; rDelta = true }
-	  lf
+          { red with rConst = union_consts red.rConst l; rDelta = true }
+          lf
   in
   add_flag
     {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []}
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index fc9f087fd..6e64e3fa6 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -185,7 +185,7 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
   List.iteri (fun i t_i ->
     if not (List.mem_assoc (i+1) li) then
       let fvs = List.map ((+) (i+1)) (Int.Set.elements (free_rels t_i)) in
-      match List.intersect fvs reversible_rels with
+      match List.intersect Int.equal fvs reversible_rels with
       | [] -> ()
       | _ -> raise Elimconst)
     labs;
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 908010428..2e2389f09 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -555,7 +555,7 @@ let free_rels m =
 let collect_metas c =
   let rec collrec acc c =
     match kind_of_term c with
-      | Meta mv -> List.add_set mv acc
+      | Meta mv -> List.add_set Int.equal mv acc
       | _       -> fold_constr collrec acc c
   in
   List.rev (collrec [] c)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index c562e6faa..b9b076d4f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -110,7 +110,9 @@ let extract_instance_status = function
 
 let rec subst_meta_instances bl c =
   match kind_of_term c with
-    | Meta i -> (try List.assoc_snd_in_triple i bl with Not_found -> c)
+    | Meta i ->
+      let select (j,_,_) = Int.equal i j in
+      (try pi2 (List.find select bl) with Not_found -> c)
     | _ -> map_constr (subst_meta_instances bl) c
 
 let pose_all_metas_as_evars env evd t =