Fixing pervasive comparisons

interp/notation.ml

@@ -116,6 +116,12 @@ let normalize_scope sc =
 type scope_elem = Scope of scope_name | SingleNotation of string
 type scopes = scope_elem list
 
+let scope_eq s1 s2 = match s1, s2 with
+| Scope s1, Scope s2
+| SingleNotation s1, SingleNotation s2 -> String.equal s1 s2
+| Scope _, SingleNotation _
+| SingleNotation _, Scope _ -> false
+
 let scope_stack = ref []
 
 let current_scopes () = !scope_stack
@@ -136,7 +142,7 @@ let open_scope i (_,(local,op,sc)) =
     in
     scope_stack :=
       if op then sc :: !scope_stack
-      else List.except Pervasives.(=) sc !scope_stack (* FIXME *)
+      else List.except scope_eq sc !scope_stack
 
 let cache_scope o =
   open_scope 1 o

interp/notation_ops.ml

@@ -512,12 +512,6 @@ let rec alpha_var id1 id2 = function
   | _::idl -> alpha_var id1 id2 idl
   | [] -> Id.equal id1 id2
 
-let compare_var v1 v2 =
-  match v1, v2 with
-  | GHole _, _ -> (true,true)
-  | _, GHole _ -> (false,false)
-  | _, _ -> (true,Pervasives.(=) v1 v2 (** FIXME *))
-
 let add_env alp (sigma,sigmalist,sigmabinders) var v =
   (* Check that no capture of binding variables occur *)
   if List.exists (fun (id,_) ->occur_glob_constr id v) alp then raise No_match;

lib/option.ml

@@ -29,6 +29,12 @@ let equal f x y = match x, y with
 | Some x, Some y -> f x y
 | _, _ -> false
 
+let compare f x y = match x, y with
+| None, None -> 0
+| Some x, Some y -> f x y
+| None, Some _ -> -1
+| Some _, None -> 1
+
 exception IsNone
 
 (** [get x] returns [y] where [x] is [Some y]. It raises IsNone

lib/option.mli

@@ -28,6 +28,9 @@ val is_empty : 'a option -> bool
     [f] is called. Otherwise it returns [false]. *)
 val equal : ('a -> 'a -> bool) -> 'a option -> 'a option -> bool
 
+(** Same as [equal], but with comparison. *)
+val compare : ('a -> 'a -> int) -> 'a option -> 'a option -> int
+
 (** [get x] returns [y] where [x] is [Some y]. It raises IsNone
     if [x] equals [None]. *)
 val get : 'a option -> 'a

library/globnames.ml

@@ -132,7 +132,8 @@ module ExtRefOrdered = struct
     match x, y with
       | TrueGlobal rx, TrueGlobal ry -> global_ord_user rx ry
       | SynDef knx, SynDef kny -> kn_ord knx kny
-      | _, _ -> Pervasives.compare x y
+      | TrueGlobal _, SynDef _ -> -1
+      | SynDef _, TrueGlobal _ -> 1
 end
 
 type global_reference_or_constr = 

library/impargs.ml

@@ -119,6 +119,13 @@ let argument_position_eq p1 p2 = match p1, p2 with
 | Hyp h1, Hyp h2 -> Int.equal h1 h2
 | _ -> false
 
+let explicitation_eq ex1 ex2 = match ex1, ex2 with
+| ExplByPos (i1, id1), ExplByPos (i2, id2) ->
+  Int.equal i1 i2 && Option.equal Id.equal id1 id2
+| ExplByName id1, ExplByName id2 ->
+  Id.equal id1 id2
+| _ -> false
+
 type implicit_explanation =
   | DepRigid of argument_position
   | DepFlex of argument_position
@@ -352,7 +359,7 @@ let set_manual_implicits env flags enriching autoimps l =
   | (Name id,imp)::imps ->
       let l',imp,m =
 	try
-          let eq = (Pervasives.(=) : explicitation -> explicitation -> bool) in (* FIXME *)
+          let eq = explicitation_eq in
 	  let (b, fi, fo) = List.assoc_f eq (ExplByName id) l in
 	  List.remove_assoc_f eq (ExplByName id) l, (Some Manual), (Some (b, fi))
 	with Not_found ->

library/impargs.mli

@@ -143,3 +143,5 @@ type implicit_discharge_request =
   | ImplInteractive of global_reference * implicits_flags *
       implicit_interactive_request
 
+val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool
+(** Equality on [explicitation]. *)

plugins/cc/ccalgo.ml

@@ -88,11 +88,11 @@ struct
   type t = pa_constructor
   let compare { cnode = cnode0; arity = arity0; args = args0 }
               { cnode = cnode1; arity = arity1; args = args1 } =
-    let cmp = Pervasives.compare cnode0 cnode1 in
+    let cmp = Int.compare cnode0 cnode1 in
     if cmp = 0 then
-      let cmp' = Pervasives.compare arity0 arity1 in
+      let cmp' = Int.compare arity0 arity1 in
       if cmp' = 0 then
-        Pervasives.compare args0 args1
+        List.compare Int.compare args0 args1
       else
         cmp'
     else
@@ -103,9 +103,9 @@ module PafOrd =
 struct
   type t = pa_fun
   let compare { fsym = fsym0; fnargs = fnargs0 } { fsym = fsym1; fnargs = fnargs1 } =
-    let cmp = Pervasives.compare fsym0 fsym1 in
+    let cmp = Int.compare fsym0 fsym1 in
     if cmp = 0 then
-      Pervasives.compare fnargs0 fnargs1
+      Int.compare fnargs0 fnargs1
     else
       cmp
 end

plugins/firstorder/sequent.ml

@@ -67,12 +67,14 @@ module Hitem=
 struct
   type t = h_item
   let compare (id1,co1) (id2,co2)=
-    (Globnames.RefOrdered.compare
-     =? (fun oc1 oc2 ->
-	   match oc1,oc2 with
-	       Some (m1,c1),Some (m2,c2) ->
-		 ((-) =? OrderedConstr.compare) m1 m2 c1 c2
-	     | _,_->Pervasives.compare oc1 oc2)) id1 id2 co1 co2
+    let c = Globnames.RefOrdered.compare id1 id2 in
+    if c = 0 then
+      let cmp (i1, c1) (i2, c2) =
+        let c = Int.compare i1 i2 in
+        if c = 0 then OrderedConstr.compare c1 c2 else c
+      in
+      Option.compare cmp co1 co2
+    else c
 end
 
 module CM=Map.Make(OrderedConstr)

plugins/funind/functional_principles_proofs.ml

@@ -288,11 +288,10 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
       (* Ugly hack to prevent Map.fold order change between ocaml-3.08.3 and ocaml-3.08.4
 	 Can be safely replaced by the next comment for Ocaml >= 3.08.4
       *)
-      let sub' = Int.Map.fold (fun i t acc -> (i,t)::acc) sub [] in
-      let sub'' = List.sort (fun (x,_) (y,_) -> Pervasives.compare x y) sub' in
+      let sub = Int.Map.bindings sub in
       List.fold_left (fun end_of_type (i,t)  -> lift 1 (substnl  [t] (i-1) end_of_type))
 	end_of_type_with_pop
-	sub''
+	sub
     in
     let old_context_length = List.length context + 1 in
     let witness_fun =

plugins/micromega/certificate.ml

@@ -313,7 +313,7 @@ let primal l =
 
   let op_op = function Mc.NonStrict -> Ge |Mc.Equal -> Eq | _ -> raise Strict in
 
-  let cmp x y = Pervasives.compare (fst x) (fst y) in
+  let cmp x y = Int.compare (fst x) (fst y) in
 
    snd (List.fold_right (fun  (p,op) (map,l) ->
       let (mp,vect) = vect_of_poly map p in  

plugins/micromega/mfourier.ml

@@ -10,6 +10,8 @@ let from_option = Utils.from_option
 let debug = false
 type ('a,'b) lr = Inl of 'a | Inr of 'b
 
+let compare_float (p : float) q = Pervasives.compare p q
+
 (** Implementation of intervals *)
 module Itv =
 struct
@@ -590,7 +592,7 @@ struct
       (ISet.fold (fun v (eval,s) -> let ts,vl = abstract_partition v s  in
                                       ((v,vl)::eval, ts)) v ([],sl)) in
 
-      List.sort (fun x y -> Pervasives.compare (snd x) (snd y) ) evals
+      List.sort (fun x y -> compare_float (snd x) (snd y) ) evals
 
 
 end
@@ -704,7 +706,7 @@ struct
 
 	      (*      pp_list (fun o ((v,eq,_,_),cst) -> Printf.fprintf o "((%i,%a),%i)\n" v pp_vect eq cst) stdout all_costs ; *)
 
-	      List.sort (fun x y -> Pervasives.compare (snd x) (snd y) ) all_costs
+	      List.sort (fun x y -> Int.compare (snd x) (snd y) ) all_costs
 	| Some (v,vect, const,prf,_) -> [(v,vect,const,prf),0]
 
 

plugins/micromega/mutils.ml

@@ -393,7 +393,7 @@ struct
   let from i = i
   let next i = i + 1
   let pp o i = output_string o (string_of_int i)
-  let compare : int -> int -> int = Pervasives.compare
+  let compare : int -> int -> int = Int.compare
 
 end
 

plugins/micromega/polynomial.ml

@@ -44,7 +44,7 @@ end
  =
 struct
  (* A monomial is represented by a multiset of variables  *)
- module Map = Map.Make(struct type t = var let compare = Pervasives.compare end)
+ module Map = Map.Make(Int)
  open Map
 
  type t = int Map.t
@@ -65,8 +65,8 @@ struct
    fun m1 m2 -> 
      let s1 = sum_degree m1 
      and s2 = sum_degree m2 in
-       if s1 = s2 then Map.compare Pervasives.compare m1 m2
-       else Pervasives.compare s1 s2
+       if Int.equal s1 s2 then Map.compare Int.compare m1 m2
+       else Int.compare s1 s2
 
  let is_const m = (m = Map.empty)
 
@@ -241,16 +241,15 @@ module Vect =
     type var = int
     type t = (var * num) list
 
-(** [equal v1 v2 = true] if the vectors are syntactically equal.
-    ([num] is not handled by  [Pervasives.equal] *)
+(** [equal v1 v2 = true] if the vectors are syntactically equal. *)
 
     let rec equal v1 v2 =
       match v1 , v2 with
 	| [] , []   -> true
 	| [] , _    -> false
 	| _::_ , [] -> false
 	| (i1,n1)::v1 , (i2,n2)::v2 ->
-	    (i1 = i2) && n1 =/ n2 && equal v1 v2
+	    (Int.equal i1 i2) && n1 =/ n2 && equal v1 v2
 
     let hash v =
       let rec hash i = function
@@ -294,7 +293,7 @@ module Vect =
       match t with
 	| [] -> cons i (f zero_num) []
 	| (k,v)::l ->
-	    match Pervasives.compare i k with
+	    match Int.compare i k with
 	  | 0 -> cons k (f v) l
 	  | -1 -> cons i (f zero_num) t
 	  |  1 -> (k,v) ::(update i f l)
@@ -304,7 +303,7 @@ module Vect =
       match t with
 	| [] -> cons i n []
 	| (k,v)::l ->
-	    match Pervasives.compare i k with
+	    match Int.compare i k with
 	      | 0 -> cons k n l
 	      | -1 -> cons i n t
 	      |  1 -> (k,v) :: (set i n l)
@@ -346,7 +345,7 @@ module Vect =
 
     let compare : t -> t -> int = Utils.Cmp.compare_list (fun x y -> Utils.Cmp.compare_lexical
       [
-	(fun () -> Pervasives.compare (fst x) (fst y));
+	(fun () -> Int.compare (fst x) (fst y));
 	(fun () -> compare_num (snd x) (snd y))])
 
     (** [tail v vect] returns
@@ -359,7 +358,7 @@ module Vect =
       match vect with
 	| [] -> None
 	| (v',vl)::vect' ->
-	    match Pervasives.compare v' v with
+	    match Int.compare v' v with
 	      | 0 -> Some (vl,vect) (* Ok, found *)
 	      | -1 -> tail v vect' (* Might be in the tail *)
 	      | _  -> None (* Hopeless *)
@@ -615,7 +614,7 @@ struct
   end 
 
   let normalise (v,c) = 
-    (List.sort  (fun x y -> Pervasives.compare (fst x) (fst y)) v , c)
+    (List.sort  (fun x y -> Int.compare (fst x) (fst y)) v , c)
 
 
   let output_mon o (x,v) = 

plugins/micromega/sos_lib.ml

@@ -15,11 +15,13 @@ let debugging = ref false;;
 (* Comparisons that are reflexive on NaN and also short-circuiting.          *)
 (* ------------------------------------------------------------------------- *)
 
-let (=?) = fun x y -> Pervasives.compare x y = 0;;
-let (<?) = fun x y -> Pervasives.compare x y < 0;;
-let (<=?) = fun x y -> Pervasives.compare x y <= 0;;
-let (>?) = fun x y -> Pervasives.compare x y > 0;;
-let (>=?) = fun x y -> Pervasives.compare x y >= 0;;
+let cmp = Pervasives.compare (** FIXME *)
+
+let (=?) = fun x y -> cmp x y = 0;;
+let (<?) = fun x y -> cmp x y < 0;;
+let (<=?) = fun x y -> cmp x y <= 0;;
+let (>?) = fun x y -> cmp x y > 0;;
+let (>=?) = fun x y -> cmp x y >= 0;;
 
 (* ------------------------------------------------------------------------- *)
 (* Combinators.                                                              *)

plugins/rtauto/proof_search.ml

@@ -69,7 +69,7 @@ module FOrd = struct
     | Bot, Bot -> 0
     | Bot, _ -> -1
     | Atom _, Bot -> 1
-    | Atom a1, Atom a2 -> Pervasives.compare a1 a2
+    | Atom a1, Atom a2 -> Int.compare a1 a2
     | Atom _, _ -> -1
     | Arrow _, (Bot | Atom _) -> 1
     | Arrow (f1, g1), Arrow (f2, g2) ->

pretyping/classops.ml

@@ -59,7 +59,7 @@ let cl_typ_ord t1 t2 = match t1, t2 with
   | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2
   | CL_CONST c1, CL_CONST c2 -> con_user_ord c1 c2
   | CL_IND i1, CL_IND i2 -> ind_user_ord i1 i2
-  | _ -> Pervasives.compare t1 t2
+  | _ -> Pervasives.compare t1 t2 (** OK *)
 
 module ClTyp = struct
   type t = cl_typ

pretyping/coercion.ml

@@ -274,7 +274,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 		       (* 			     else subco () *)
 		 else
 		   subco ()
-	   | x, y when Pervasives.(=) x y -> (** FIXME *)
+	   | x, y when Constr.equal c c' ->
 	       if Int.equal (Array.length l) (Array.length l') then
 		 let evm =  !evdref in
 		 let lam_type = Typing.type_of env evm c in

pretyping/recordops.ml

@@ -144,6 +144,21 @@ type cs_pattern =
   | Sort_cs of sorts_family
   | Default_cs
 
+let eq_obj_typ o1 o2 =
+  Constr.equal o1.o_DEF o2.o_DEF &&
+  Int.equal o1.o_INJ o2.o_INJ &&
+  List.equal Constr.equal o1.o_TABS o2.o_TABS &&
+  List.equal Constr.equal o1.o_TPARAMS o2.o_TPARAMS &&
+  Int.equal o1.o_NPARAMS o2.o_NPARAMS &&
+  List.equal Constr.equal o1.o_TCOMPS o2.o_TCOMPS
+
+let eq_cs_pattern p1 p2 = match p1, p2 with
+| Const_cs gr1, Const_cs gr2 -> eq_gr gr1 gr2
+| Prod_cs, Prod_cs -> true
+| Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2
+| Default_cs, Default_cs -> true
+| _ -> false
+
 let object_table =
   Summary.ref (Refmap.empty : (cs_pattern * obj_typ) list Refmap.t)
     ~name:"record-canonical-structs"
@@ -221,7 +236,7 @@ let open_canonical_structure i (_,o) =
     let lo = compute_canonical_projections o in
     List.iter (fun ((proj,cs_pat),s) ->
       let l = try Refmap.find proj !object_table with Not_found -> [] in
-      let ocs = try Some (List.assoc_f Pervasives.(=) cs_pat l) (* FIXME *)
+      let ocs = try Some (List.assoc_f eq_cs_pattern cs_pat l)
       with Not_found -> None
       in match ocs with
         | None -> object_table := Refmap.add proj ((cs_pat,s)::l) !object_table;
@@ -287,7 +302,7 @@ let declare_canonical_structure ref =
   add_canonical_structure (check_and_decompose_canonical_structure ref)
 
 let lookup_canonical_conversion (proj,pat) =
-  List.assoc_f Pervasives.(=) pat (Refmap.find proj !object_table) (* FIXME *)
+  List.assoc_f eq_cs_pattern pat (Refmap.find proj !object_table)
 
 let is_open_canonical_projection env sigma (c,args) =
   try

proofs/clenv.ml

@@ -378,8 +378,13 @@ let clenv_independent clenv =
   let deps = Metaset.union (dependent_in_type_of_metas clenv mvs) ctyp_mvs in
   List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
 
+let qhyp_eq h1 h2 = match h1, h2 with
+| NamedHyp n1, NamedHyp n2 -> Id.equal n1 n2
+| AnonHyp i1, AnonHyp i2 -> Int.equal i1 i2
+| _ -> false
+
 let check_bindings bl =
-  match List.duplicates Pervasives.(=) (List.map pi2 bl) with (* FIXME *)
+  match List.duplicates qhyp_eq (List.map pi2 bl) with
     | NamedHyp s :: _ ->
 	errorlabstrm ""
 	  (str "The variable " ++ pr_id s ++

tactics/equality.ml

@@ -1126,7 +1126,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
 let make_iterated_tuple env sigma dflt (z,zty) =
   let (zty,rels) = minimal_free_rels_rec env sigma (z,zty) in
   let sort_of_zty = get_sort_of env sigma zty in
-  let sorted_rels = List.sort Pervasives.compare (Int.Set.elements rels) in
+  let sorted_rels = Int.Set.elements rels in
   let (tuple,tuplety) =
     List.fold_left (make_tuple env sigma) (z,zty) sorted_rels
   in