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

5 files changed, 40 insertions, 32 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 13816d1db..95aaf4518 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1587,7 +1587,7 @@ let prove_principle_for_gen
 	  Elim.h_decompose_and (mkVar hid);
 	  (fun g ->
 	     let new_hyps = pf_ids_of_hyps g in
-	     tcc_list := List.rev (List.subtract new_hyps (hid::hyps));
+	     tcc_list := List.rev (List.subtract Id.equal new_hyps (hid::hyps));
 	     if List.is_empty !tcc_list
 	     then
 	       begin
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 2cc203ed5..91ea714c1 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -90,7 +90,7 @@ let combine_results
   in (* and then we flatten the map *)
   {
     result = List.concat pre_result;
-    to_avoid = List.union res1.to_avoid res2.to_avoid
+    to_avoid = List.union Id.equal res1.to_avoid res2.to_avoid
   }
 
 
@@ -711,7 +711,8 @@ and build_entry_lc_from_case env funname make_discr
 	{
 	  result = List.concat (List.map (fun r -> r.result) results);
 	  to_avoid =
-	    List.fold_left (fun acc r -> List.union acc r.to_avoid) [] results
+	    List.fold_left (fun acc r -> List.union Id.equal acc r.to_avoid)
+              [] results
 	}
 
 and build_entry_lc_from_case_term env types funname make_discr patterns_to_prevent brl avoid
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 22e82035b..96a60424c 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1276,7 +1276,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 		    (Elim.h_decompose_and (mkVar hid))
 		    (fun g ->
 		       let ids' = pf_ids_of_hyps g in
-		       lid := List.rev (List.subtract ids' ids);
+		       lid := List.rev (List.subtract Id.equal ids' ids);
 		       if List.is_empty !lid then lid := [hid];
 		       tclIDTAC g
 		    )
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index 60887b451..cf1a7e6db 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -19,6 +19,7 @@
 
 module type INT = sig
   type bigint
+  val equal : bigint -> bigint -> bool
   val less_than : bigint -> bigint -> bool
   val add : bigint -> bigint -> bigint
   val sub : bigint -> bigint -> bigint
@@ -32,26 +33,26 @@ end
 
 let debug = ref false
 
-module MakeOmegaSolver (Int:INT) = struct
-
-type bigint = Int.bigint
-let (<?) = Int.less_than
-let (<=?) x y = Int.less_than x y || x = y
-let (>?) x y = Int.less_than y x
-let (>=?) x y = Int.less_than y x || x = y
-let (=?) = (=)
-let (+) = Int.add
-let (-) = Int.sub
-let ( * ) = Int.mult
-let (/) x y = fst (Int.euclid x y)
-let (mod) x y = snd (Int.euclid x y)
-let zero = Int.zero
-let one = Int.one
+module MakeOmegaSolver (I:INT) = struct
+
+type bigint = I.bigint
+let (=?) = I.equal
+let (<?) = I.less_than
+let (<=?) x y = I.less_than x y || x = y
+let (>?) x y = I.less_than y x
+let (>=?) x y = I.less_than y x || x = y
+let (+) = I.add
+let (-) = I.sub
+let ( * ) = I.mult
+let (/) x y = fst (I.euclid x y)
+let (mod) x y = snd (I.euclid x y)
+let zero = I.zero
+let one = I.one
 let two = one + one
-let negone = Int.neg one
-let abs x = if Int.less_than x zero then Int.neg x else x
-let string_of_bigint = Int.to_string
-let neg = Int.neg
+let negone = I.neg one
+let abs x = if I.less_than x zero then I.neg x else x
+let string_of_bigint = I.to_string
+let neg = I.neg
 
 (* To ensure that polymorphic (<) is not used mistakenly on big integers *)
 (* Warning: do not use (=) either on big int *)
@@ -697,14 +698,16 @@ let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system =
           | [] -> failwith "solve" in
         let s1,s2 =
           List.partition (fun (_,_,decomp,_) -> sign decomp) systems in
-        let s1' =
-	  List.map (fun (dep,ro,dc,pa) -> (Util.List.except id dep,ro,dc,pa)) s1 in
-        let s2' =
-	  List.map (fun (dep,ro,dc,pa) -> (Util.List.except id dep,ro,dc,pa)) s2 in
+        let remove_int (dep,ro,dc,pa) =
+          (Util.List.except Int.equal id dep,ro,dc,pa)
+        in
+        let s1' = List.map remove_int s1 in
+        let s2' = List.map remove_int s2 in
         let (r1,relie1) = solve s1'
 	and (r2,relie2) = solve s2' in
 	let (eq,id1,id2) = List.assoc id explode_map in
-	[SPLIT_INEQ(eq,(id1,r1),(id2, r2))], eq.id :: Util.List.union relie1 relie2
+	[SPLIT_INEQ(eq,(id1,r1),(id2, r2))],
+        eq.id :: Util.List.union Int.equal relie1 relie2
       with FULL_SOLUTION (x0,x1) -> (x0,x1)
     in
     let act,relie_on = solve all_solutions in
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 635fc366f..752fa4598 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -921,7 +921,7 @@ let add_stated_equations env tree =
 let rec get_eclatement env = function
     i :: r ->
       let l = try (get_equation env i).e_depends with Not_found -> [] in
-      List.union (List.rev l) (get_eclatement env r)
+      List.union Pervasives.(=) (List.rev l) (get_eclatement env r)
   | [] -> []
 
 let select_smaller l =
@@ -1207,12 +1207,16 @@ let resolution env full_reified_goal systems_list =
   (* recupere explicitement ces equations *)
   let equations = List.map (get_equation env) useful_equa_id in
   let l_hyps' = List.uniquize (List.map (fun e -> e.e_origin.o_hyp) equations) in
-  let l_hyps = id_concl :: List.remove id_concl l_hyps' in
+  let l_hyps = id_concl :: List.remove Names.Id.equal id_concl l_hyps' in
   let useful_hyps =
-    List.map (fun id -> List.assoc id full_reified_goal) l_hyps in
+    List.map
+      (fun id -> List.assoc_f Names.Id.equal id full_reified_goal) l_hyps
+  in
   let useful_vars =
     let really_useful_vars = vars_of_equations equations in
-    let concl_vars = vars_of_prop (List.assoc id_concl full_reified_goal) in
+    let concl_vars =
+      vars_of_prop (List.assoc_f Names.Id.equal id_concl full_reified_goal)
+    in
     really_useful_vars @@ concl_vars
   in
   (* variables a introduire *)