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

30 files changed, 177 insertions, 153 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 6ea1678ac..eb09d3bbb 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -67,7 +67,7 @@ end = struct
   let hidden_edit_id () = decr id; !id
 
   let set_flags s f = s.flags <- f
-  let add_flag s f = s.flags <- CList.add_set f s.flags
+  let add_flag s f = s.flags <- CList.add_set (=) f s.flags
   let has_flag s mf =
     List.exists (fun f -> mem_flag_of_flag f = mf) s.flags
   let remove_flag s mf =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 51c8e2e10..74a49152c 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -833,7 +833,7 @@ let check_number_of_pattern loc n l =
   if not (Int.equal n p) then raise (InternalizationError (loc,BadPatternsNumber (n,p)))
 
 let check_or_pat_variables loc ids idsl =
-  if List.exists (fun ids' -> not (List.eq_set ids ids')) idsl then
+  if List.exists (fun ids' -> not (List.eq_set Id.equal ids ids')) idsl then
     user_err_loc (loc, "", str
     "The components of this disjunctive pattern must bind the same variables.")
 
diff --git a/interp/notation.ml b/interp/notation.ml
index 2363789fa..b661c33c6 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -135,7 +135,8 @@ let open_scope i (_,(local,op,sc)) =
       | _ -> sc
     in
     scope_stack :=
-      if op then sc :: !scope_stack else List.except sc !scope_stack
+      if op then sc :: !scope_stack
+      else List.except Pervasives.(=) sc !scope_stack (* FIXME *)
 
 let cache_scope o =
   open_scope 1 o
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index 88c99683e..d2469c4fd 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -44,6 +44,8 @@ let family = function
   | Prop Pos -> InSet
   | Type _ -> InType
 
+let family_equal = (==)
+
 module Hsorts =
   Hashcons.Make(
     struct
diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index f15b7cba4..51e8a6f6c 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -27,3 +27,5 @@ val is_prop : t -> bool
 val family : t -> family
 
 val hcons : t -> t
+
+val family_equal : family -> family -> bool
diff --git a/kernel/univ.ml b/kernel/univ.ml
index ddb5dcbc6..aa6c9c4c8 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -154,12 +154,12 @@ let sup u v =
 	if UniverseLevel.equal u v then Atom u else Max ([u;v],[])
     | u, Max ([],[]) -> u
     | Max ([],[]), v -> v
-    | Atom u, Max (gel,gtl) -> Max (List.add_set u gel,gtl)
-    | Max (gel,gtl), Atom v -> Max (List.add_set v gel,gtl)
+    | Atom u, Max (gel,gtl) -> Max (List.add_set UniverseLevel.equal u gel,gtl)
+    | Max (gel,gtl), Atom v -> Max (List.add_set UniverseLevel.equal v gel,gtl)
     | Max (gel,gtl), Max (gel',gtl') ->
-	let gel'' = List.union gel gel' in
-	let gtl'' = List.union gtl gtl' in
-	Max (List.subtract gel'' gtl'',gtl'')
+	let gel'' = List.union UniverseLevel.equal gel gel' in
+	let gtl'' = List.union UniverseLevel.equal gtl gtl' in
+	Max (List.subtract UniverseLevel.equal gel'' gtl'',gtl'')
 
 (* Comparison on this type is pointer equality *)
 type canonical_arc =
@@ -865,11 +865,11 @@ let make_max = function
 
 let remove_large_constraint u = function
   | Atom u' as x -> if UniverseLevel.equal u u' then Max ([],[]) else x
-  | Max (le,lt) -> make_max (List.remove u le,lt)
+  | Max (le,lt) -> make_max (List.remove UniverseLevel.equal u le,lt)
 
 let is_direct_constraint u = function
   | Atom u' -> UniverseLevel.equal u u'
-  | Max (le,lt) -> List.mem u le
+  | Max (le,lt) -> List.mem_f UniverseLevel.equal u le
 
 (*
    Solve a system of universe constraint of the form
diff --git a/lib/cList.ml b/lib/cList.ml
index 2cc5e4cfd..904f3ee63 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -6,6 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
+type 'a cmp = 'a -> 'a -> int
+type 'a eq = 'a -> 'a -> bool
+
 module type S =
 sig
   val length : 'a list -> int
@@ -54,22 +57,23 @@ end
 module type ExtS =
 sig
   include S
-  val compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int
-  val equal : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
+  val compare : 'a cmp -> 'a list cmp
+  val equal : 'a eq -> 'a list eq
   val is_empty : 'a list -> bool
   val init : int -> (int -> 'a) -> 'a list
-  val add_set : 'a -> 'a list -> 'a list
-  val eq_set : 'a list -> 'a list -> bool
-  val intersect : 'a list -> 'a list -> 'a list
-  val union : 'a list -> 'a list -> 'a list
+  val mem_f : 'a eq -> 'a -> 'a list -> bool
+  val add_set : 'a eq -> 'a -> 'a list -> 'a list
+  val eq_set : 'a eq -> 'a list -> 'a list -> bool
+  val intersect : 'a eq -> 'a list -> 'a list -> 'a list
+  val union : 'a eq -> 'a list -> 'a list -> 'a list
   val unionq : 'a list -> 'a list -> 'a list
-  val subtract : 'a list -> 'a list -> 'a list
+  val subtract : 'a eq -> 'a list -> 'a list -> 'a list
   val subtractq : 'a list -> 'a list -> 'a list
   val interval : int -> int -> int list
   val make : int -> 'a -> 'a list
   val assign : 'a list -> int -> 'a -> 'a list
   val distinct : 'a list -> bool
-  val duplicates : 'a list -> 'a list
+  val duplicates : 'a eq -> 'a list -> 'a list
   val filter2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
   val map_filter : ('a -> 'b option) -> 'a list -> 'b list
   val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list
@@ -98,11 +102,9 @@ sig
       ('a -> 'b -> 'b list -> 'a) -> 'b list -> 'a -> 'a
   val fold_left3 : ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b list -> 'c list -> 'd list -> 'a
   val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
-  val except : 'a -> 'a list -> 'a list
-  val remove : 'a -> 'a list -> 'a list
-  val remove_first : 'a -> 'a list -> 'a list
-  val remove_assoc_in_triple : 'a -> ('a * 'b * 'c) list -> ('a * 'b * 'c) list
-  val assoc_snd_in_triple : 'a -> ('a * 'b * 'c) list -> 'b
+  val except : 'a eq -> 'a -> 'a list -> 'a list
+  val remove : 'a eq -> 'a -> 'a list -> 'a list
+  val remove_first : ('a -> bool) -> 'a list -> 'a list
   val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
   val sep_last : 'a list -> 'a * 'a list
   val find_map : ('a -> 'b option) -> 'a list -> 'b
@@ -127,7 +129,8 @@ sig
   val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
   val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
   val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
-  val assoc_f : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> 'b
+  val assoc_f : 'a eq -> 'a -> ('a * 'b) list -> 'b
+  val remove_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> ('a * 'b) list
   val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   val cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
   val combinations : 'a list list -> 'a list list
@@ -316,28 +319,24 @@ let is_empty = function
 | [] -> true
 | _ -> false
 
-let intersect l1 l2 =
-  filter (fun x -> List.mem x l2) l1
+let mem_f cmp x l = List.exists (cmp x) l
 
-let union l1 l2 =
-  let rec urec = function
-    | [] -> l2
-    | a::l -> if List.mem a l2 then urec l else a::urec l
-  in
-  urec l1
+let intersect cmp l1 l2 =
+  filter (fun x -> mem_f cmp x l2) l1
 
-let unionq l1 l2 =
+let union cmp l1 l2 =
   let rec urec = function
     | [] -> l2
-    | a::l -> if List.memq a l2 then urec l else a::urec l
+    | a::l -> if mem_f cmp a l2 then urec l else a::urec l
   in
   urec l1
 
-let subtract l1 l2 =
-  if l2 = [] then l1 else List.filter (fun x -> not (List.mem x l2)) l1
+let subtract cmp l1 l2 =
+  if is_empty l2 then l1
+  else List.filter (fun x -> not (mem_f cmp x l2)) l1
 
-let subtractq l1 l2 =
-  if l2 = [] then l1 else List.filter (fun x -> not (List.memq x l2)) l1
+let unionq l1 l2 = union (==) l1 l2
+let subtractq l1 l2 = subtract (==) l1 l2
 
 let tabulate = init
 
@@ -416,14 +415,9 @@ let index_f f x =
 
 let index0_f f x l = index_f f x l - 1
 
-let index x =
-  let rec index_x n = function
-    | y::l -> if x = y then n else index_x (succ n) l
-    | [] -> raise Not_found
-  in
-  index_x 1
+let index x l = index_f Pervasives.(=) x l (* FIXME : prefer [index_f]*)
 
-let index0 x l = index x l - 1
+let index0 x l = index x l - 1 (* FIXME *)
 
 let fold_left_until f accu s =
   let rec aux accu = function
@@ -478,29 +472,23 @@ let for_all_i p =
   in
   for_all_p
 
-let except x l = List.filter (fun y -> not (x = y)) l
+let except cmp x l = List.filter (fun y -> not (cmp x y)) l
 
 let remove = except (* Alias *)
 
-let rec remove_first a = function
-  | b::l when a = b -> l
-  | b::l -> b::remove_first a l
+let rec remove_first p = function
+  | b::l when p b -> l
+  | b::l -> b::remove_first p l
   | [] -> raise Not_found
 
-let rec remove_assoc_in_triple x = function
-  | [] -> []
-  | (y,_,_ as z)::l -> if x = y then l else z::remove_assoc_in_triple x l
-
-let rec assoc_snd_in_triple x = function
-    [] -> raise Not_found
-  | (a,b,_)::l -> if Int.equal (Pervasives.compare a x) 0 then b else assoc_snd_in_triple x l
+let add_set cmp x l = if mem_f cmp x l then l else x :: l
 
-let add_set x l = if List.mem x l then l else x :: l
+(** List equality up to permutation (but considering multiple occurrences) *)
 
-let eq_set l1 l2 =
+let eq_set cmp l1 l2 =
   let rec aux l1 = function
-  | [] -> l1 = []
-  | a::l2 -> aux (remove_first a l1) l2 in
+  | [] -> is_empty l1
+  | a::l2 -> aux (remove_first (cmp a) l1) l2 in
   try aux l1 l2 with Not_found -> false
 
 let for_all2eq f l1 l2 =
@@ -561,11 +549,11 @@ let rec merge_uniq cmp l1 l2 =
       then h1 :: merge_uniq cmp t1 l2
       else h2 :: merge_uniq cmp l1 t2
 
-let rec duplicates = function
+let rec duplicates cmp = function
   | [] -> []
   | x::l ->
-      let l' = duplicates l in
-      if List.mem x l then add_set x l' else l'
+      let l' = duplicates cmp l in
+      if mem_f cmp x l then add_set cmp x l' else l'
 
 let rec filter2_loop f p q l1 l2 = match l1, l2 with
 | [], [] -> ()
@@ -673,7 +661,7 @@ let skipn_at_least n l =
 
 let prefix_of prefl l =
   let rec prefrec = function
-    | (h1::t1, h2::t2) -> h1 = h2 && prefrec (t1,t2)
+    | (h1::t1, h2::t2) -> h1 = h2 && prefrec (t1,t2) (* FIXME *)
     | ([], _) -> true
     | (_, _) -> false
   in
@@ -685,7 +673,7 @@ let drop_prefix p l =
     | ([], tl) -> Some tl
     | (_, []) -> None
     | (h1::tp, h2::tl) ->
-        if h1 = h2 then drop_prefix_rec (tp,tl) else None
+        if h1 = h2 then drop_prefix_rec (tp,tl) else None (* FIXME *)
   in
     match drop_prefix_rec (p,l) with
       | Some r -> r
@@ -729,6 +717,8 @@ let rec assoc_f f a = function
   | (x, e) :: xs -> if f a x then e else assoc_f f a xs
   | [] -> raise Not_found
 
+let remove_assoc_f f a l = remove_first (fun (x,y) -> f a x) l
+
 (* A generic cartesian product: for any operator (**),
    [cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]],
    and so on if there are more elements in the lists. *)
@@ -770,7 +760,7 @@ let rec drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> h
 (* Factorize lists of pairs according to the left argument *)
 let rec factorize_left = function
   | (a,b)::l ->
-      let al,l' = partition (fun (a',b) -> a=a') l in
+      let al,l' = partition (fun (a',b) -> a=a') l in (* FIXME *)
       (a,(b::List.map snd al)) :: factorize_left l'
   | [] ->
       []
diff --git a/lib/cList.mli b/lib/cList.mli
index d891403d8..ee6595632 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -8,6 +8,9 @@
 
 (** FIXME: From OCaml 3.12 onwards, that would only be a [module type of] *)
 
+type 'a cmp = 'a -> 'a -> int
+type 'a eq = 'a -> 'a -> bool
+
 (** Module type [S] is the one from OCaml Stdlib. *)
 module type S =
 sig
@@ -57,10 +60,11 @@ end
 module type ExtS =
 sig
   include S
-  val compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int
+
+  val compare : 'a cmp -> 'a list cmp
   (** Lexicographic order on lists. *)
 
-  val equal : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
+  val equal : 'a eq -> 'a list eq
   (** Lifts equality to list type. *)
 
   val is_empty : 'a list -> bool
@@ -69,17 +73,20 @@ sig
   val init : int -> (int -> 'a) -> 'a list
   (** [init n f] constructs the list [f 0; ... ; f (n - 1)]. *)
 
-  val add_set : 'a -> 'a list -> 'a list
+  val mem_f : 'a eq -> 'a -> 'a list -> bool
+  (* Same as [List.mem], for some specific equality *)
+
+  val add_set : 'a eq -> 'a -> 'a list -> 'a list
   (** [add_set x l] adds [x] in [l] if it is not already there, or returns [l]
       otherwise. *)
 
-  val eq_set : 'a list -> 'a list -> bool
-  (** Test equality up to permutation. *)
+  val eq_set : 'a eq -> 'a list eq
+  (** Test equality up to permutation (but considering multiple occurrences) *)
 
-  val intersect : 'a list -> 'a list -> 'a list
-  val union : 'a list -> 'a list -> 'a list
+  val intersect : 'a eq -> 'a list -> 'a list -> 'a list
+  val union : 'a eq -> 'a list -> 'a list -> 'a list
   val unionq : 'a list -> 'a list -> 'a list
-  val subtract : 'a list -> 'a list -> 'a list
+  val subtract : 'a eq -> 'a list -> 'a list -> 'a list
   val subtractq : 'a list -> 'a list -> 'a list
 
   val interval : int -> int -> int list
@@ -96,7 +103,7 @@ sig
   val distinct : 'a list -> bool
   (** Return [true] if all elements of the list are distinct. *)
 
-  val duplicates : 'a list -> 'a list
+  val duplicates : 'a eq -> 'a list -> 'a list
   (** Return the list of unique elements which appear at least twice. Elements
       are kept in the order of their first appearance. *)
 
@@ -133,12 +140,12 @@ sig
   val index : 'a -> 'a list -> int
   (** [index] returns the 1st index of an element in a list (counting from 1). *)
 
-  val index_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int
+  val index_f : 'a eq -> 'a -> 'a list -> int
 
   val index0 : 'a -> 'a list -> int
   (** [index0] behaves as [index] except that it starts counting at 0. *)
 
-  val index0_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int
+  val index0_f : 'a eq -> 'a -> 'a list -> int
 
   val iteri :  (int -> 'a -> unit) -> 'a list -> unit
   (** As [iter] but with the index argument (starting from 0). *)
@@ -153,11 +160,9 @@ sig
       ('a -> 'b -> 'b list -> 'a) -> 'b list -> 'a -> 'a
   val fold_left3 : ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b list -> 'c list -> 'd list -> 'a
   val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
-  val except : 'a -> 'a list -> 'a list
-  val remove : 'a -> 'a list -> 'a list
-  val remove_first : 'a -> 'a list -> 'a list
-  val remove_assoc_in_triple : 'a -> ('a * 'b * 'c) list -> ('a * 'b * 'c) list
-  val assoc_snd_in_triple : 'a -> ('a * 'b * 'c) list -> 'b
+  val except : 'a eq -> 'a -> 'a list -> 'a list
+  val remove : 'a eq -> 'a -> 'a list -> 'a list
+  val remove_first : ('a -> bool) -> 'a list -> 'a list
   val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
   val sep_last : 'a list -> 'a * 'a list
 
@@ -168,7 +173,7 @@ sig
   val uniquize : 'a list -> 'a list
   (** Return the list of elements without duplicates. *)
 
-  val merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
+  val merge_uniq : 'a cmp -> 'a list -> 'a list -> 'a list
   (** Merge two sorted lists and preserves the uniqueness property. *)
 
   val subset : 'a list -> 'a list -> bool
@@ -208,7 +213,8 @@ sig
 
   val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
   val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
-  val assoc_f : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> 'b
+  val assoc_f : 'a eq -> 'a -> ('a * 'b) list -> 'b
+  val remove_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> ('a * 'b) list
 
   val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   (** A generic cartesian product: for any operator (**),
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 *)
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 =
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 5066a7b6e..dba047aa7 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -92,7 +92,7 @@ let print_impargs_by_name max = function
 let print_one_impargs_list l =
   let imps = List.filter is_status_implicit l in
   let maximps = List.filter Impargs.maximal_insertion_of imps in
-  let nonmaximps = List.subtract imps maximps in
+  let nonmaximps = List.subtract Pervasives.(=) imps maximps in (* FIXME *)
   print_impargs_by_name false nonmaximps @
   print_impargs_by_name true maximps
 
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index b75c67529..0df882b2b 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -379,7 +379,7 @@ let clenv_independent clenv =
   List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
 
 let check_bindings bl =
-  match List.duplicates (List.map pi2 bl) with
+  match List.duplicates Pervasives.(=) (List.map pi2 bl) with (* FIXME *)
     | NamedHyp s :: _ ->
 	errorlabstrm ""
 	  (str "The variable " ++ pr_id s ++
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 66e251d55..583fcf553 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -200,7 +200,10 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
   let hyps:Context.named_context list =
     List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in
   let newhyps =
-    List.map (fun hypl -> List.subtract hypl oldhyps) hyps in
+    List.map
+      (fun hypl -> List.subtract Context.eq_named_declaration hypl oldhyps)
+      hyps
+  in
   let emacs_str s =
     if !Flags.print_emacs then s else "" in
   let s = 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 373a0bb62..6050fdc9a 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1352,7 +1352,7 @@ and trivial_resolve dbg mod_delta db_list local_db cl =
 
 let make_db_list dbnames =
   let use_core = not (List.mem "nocore" dbnames) in
-  let dbnames = List.remove "nocore" dbnames in
+  let dbnames = List.remove String.equal "nocore" dbnames in
   let dbnames = if use_core then "core"::dbnames else dbnames in
   let lookup db =
     try searchtable_map db with Not_found -> error_no_such_hint_database db
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f5af80b0d..9bc86a0b9 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -430,7 +430,7 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
 	  (* If the term to rewrite uses an hypothesis H, don't rewrite in H *)
 	  let ids =
 	    let ids_in_c = Environ.global_vars_set (Global.env()) (fst c) in
-	      Id.Set.fold (fun id l -> List.remove id l) ids_in_c (pf_ids_of_hyps gl)
+	      Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c (pf_ids_of_hyps gl)
 	  in do_hyps_atleastonce ids gl
 	in
 	if cl.concl_occs == NoOccurrences then do_hyps else
@@ -565,7 +565,9 @@ let find_positions env sigma t1 t2 =
       | Construct sp1, Construct sp2
           when Int.equal (List.length args1) (mis_constructor_nargs_env env sp1)
             ->
-	  let sorts = List.intersect sorts (allowed_sorts env (fst sp1)) in
+	  let sorts =
+            List.intersect Sorts.family_equal sorts (allowed_sorts env (fst sp1))
+          in
           (* both sides are fully applied constructors, so either we descend,
              or we can discriminate here. *)
 	  if is_conv env sigma hd1 hd2 then
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2a00f7def..190c1ba58 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1393,7 +1393,8 @@ and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps =
           db_matched_hyp (curr_debug ist) (pf_env goal) hyp_match hypname;
 	  try
             let id_match = pi1 hyp_match in
-            let nextlhyps = List.remove_assoc_in_triple id_match lhyps_rest in
+            let select_match (id,_,_) = Id.equal id id_match in
+            let nextlhyps = List.remove_first select_match lhyps_rest in
             let lfun = lfun +++ lids in
             apply_hyps_context_rec lfun s.e_sub nextlhyps tl
           with e when is_match_catchable e ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 298d26915..2505a43ad 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -889,7 +889,7 @@ let clenv_fchain_in id ?(flags=elim_flags) mv elimclause hypclause =
 let elimination_in_clause_scheme with_evars ?(flags=elim_flags) id i elimclause indclause gl =
   let indmv = destMeta (nth_arg i elimclause.templval.rebus) in
   let hypmv =
-    try match List.remove indmv (clenv_independent elimclause) with
+    try match List.remove Int.equal indmv (clenv_independent elimclause) with
       | [a] -> a
       | _ -> failwith ""
     with Failure _ -> errorlabstrm "elimination_clause"
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 1dbdcf78c..127d1d76e 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -260,17 +260,17 @@ let minductive_message = function
 let check_all_names_different indl =
   let ind_names = List.map (fun ind -> ind.ind_name) indl in
   let cstr_names = List.map_append (fun ind -> List.map fst ind.ind_lc) indl in
-  let l = List.duplicates ind_names in
+  let l = List.duplicates Id.equal ind_names in
   let () = match l with
   | [] -> ()
   | t :: _ -> raise (InductiveError (SameNamesTypes t))
   in
-  let l = List.duplicates cstr_names in
+  let l = List.duplicates Id.equal cstr_names in
   let () = match l with
   | [] -> ()
   | c :: _ -> raise (InductiveError (SameNamesConstructors (List.hd l)))
   in
-  let l = List.intersect ind_names cstr_names in
+  let l = List.intersect Id.equal ind_names cstr_names in
   match l with
   | [] -> ()
   | _ -> raise (InductiveError (SameNamesOverlap l))
@@ -436,36 +436,37 @@ let do_mutual_inductive indl finite =
    partial_order : ('a * 'a list) list -> ('a * ('a,'a list) union) list
 *)
 
-let rec partial_order = function
+let rec partial_order cmp = function
   | [] -> []
   | (x,xge)::rest ->
     let rec browse res xge' = function
     | [] ->
 	let res = List.map (function
-	  | (z, Inr zge) when List.mem x zge -> (z, Inr (List.union zge xge'))
+	  | (z, Inr zge) when List.mem_f cmp x zge ->
+            (z, Inr (List.union cmp zge xge'))
 	  | r -> r) res in
 	(x,Inr xge')::res
     | y::xge ->
       let rec link y =
-	try match List.assoc y res with
+	try match List.assoc_f cmp y res with
 	| Inl z -> link z
 	| Inr yge ->
-	  if List.mem x yge then
-	    let res = List.remove_assoc y res in
+	  if List.mem_f cmp x yge then
+	    let res = List.remove_assoc_f cmp y res in
 	    let res = List.map (function
 	      | (z, Inl t) ->
-		  if Id.equal t y then (z, Inl x) else (z, Inl t)
+		  if cmp t y then (z, Inl x) else (z, Inl t)
 	      | (z, Inr zge) ->
-		  if List.mem y zge then
-		    (z, Inr (List.add_set x (List.remove y zge)))
+		  if List.mem_f cmp y zge then
+		    (z, Inr (List.add_set cmp x (List.remove cmp y zge)))
 		  else
 		    (z, Inr zge)) res in
-	    browse ((y,Inl x)::res) xge' (List.union xge (List.remove x yge))
+	    browse ((y,Inl x)::res) xge' (List.union cmp xge (List.remove cmp x yge))
 	  else
-	    browse res (List.add_set y (List.union xge' yge)) xge
-	with Not_found -> browse res (List.add_set y xge') xge
+	    browse res (List.add_set cmp y (List.union cmp xge' yge)) xge
+	with Not_found -> browse res (List.add_set cmp y xge') xge
       in link y
-    in browse (partial_order rest) [] xge
+    in browse (partial_order cmp rest) [] xge
 
 let non_full_mutual_message x xge y yge isfix rest =
   let reason =
@@ -490,7 +491,7 @@ let check_mutuality env isfix fixl =
     List.map (fun (id,def) ->
       (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env id' def) names))
       fixl in
-  let po = partial_order preorder in
+  let po = partial_order Id.equal preorder in
   match List.filter (function (_,Inr _) -> true | _ -> false) po with
     | (x,Inr xge)::(y,Inr yge)::rest ->
 	msg_warning (non_full_mutual_message x xge y yge isfix rest)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index e9fd0620d..231f764c5 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -391,7 +391,7 @@ let analyze_notation_tokens l =
   let l = raw_analyze_notation_tokens l in
   let vars = get_notation_vars l in
   let recvars,l = interp_list_parser [] l in
-  recvars, List.subtract vars (List.map snd recvars), l
+  recvars, List.subtract Id.equal vars (List.map snd recvars), l
 
 let error_not_same_scope x y =
   error ("Variables "^Id.to_string x^" and "^Id.to_string y^
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index eb4038721..fd4ac4890 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -171,8 +171,8 @@ let print_modules () =
   and loaded = Library.loaded_libraries () in
   (* we intersect over opened to preserve the order of opened since *)
   (* non-commutative operations (e.g. visibility) are done at import time *)
-  let loaded_opened = List.intersect opened loaded
-  and only_loaded = List.subtract loaded opened in
+  let loaded_opened = List.intersect DirPath.equal opened loaded
+  and only_loaded = List.subtract DirPath.equal loaded opened in
   str"Loaded and imported library files: " ++
   pr_vertical_list pr_dirpath loaded_opened ++ fnl () ++
   str"Loaded and not imported library files: " ++