Removing a bunch of generic equalities.

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

4 files changed, 11 insertions, 9 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 06058dfe4..956e777b2 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -104,7 +104,7 @@ struct
   type t = cl_index * cl_index
   let compare (i1, j1) (i2, j2) =
     let c = Int.compare i1 i2 in
-    if c = 0 then Int.compare j1 j2 else c
+    if Int.equal c 0 then Int.compare j1 j2 else c
 end
 
 module ClPairMap = Map.Make(ClPairOrd)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index ded8314dd..b4388ff08 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -640,7 +640,7 @@ let apply_on_subterm evdref f c t =
       match kind_of_term t with
       | Evar (evk,args) when Evd.is_undefined !evdref evk ->
           let ctx = evar_filtered_context (Evd.find_undefined !evdref evk) in
-          let g (_,b,_) a = if b = None then applyrec kc a else a in
+          let g (_,b,_) a = if Option.is_empty b then applyrec kc a else a in
           mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args)))
       | _ ->
         map_constr_with_binders_left_to_right (fun d (k,c) -> (k+1,lift 1 c))
@@ -653,7 +653,7 @@ let filter_possible_projections c ty ctxt args =
   let fv2 = collect_vars c in
   let tyvars = collect_vars ty in
   List.map2 (fun (id,b,_) a ->
-    b <> None ||
+    not (Option.is_empty b) ||
     a == c ||
     (* Here we make an approximation, for instance, we could also be *)
     (* interested in finding a term u convertible to c such that a occurs *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index df0187f73..c8122c4dc 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -788,7 +788,7 @@ let closure_of_filter evd evk = function
   | Some filter ->
   let evi = Evd.find_undefined evd evk in
   let vars = collect_vars (Evarutil.nf_evar evd (evar_concl evi)) in
-  let test (id,c,_) b = b || Idset.mem id vars || c <> None in
+  let test (id,c,_) b = b || Idset.mem id vars || not (Option.is_empty c) in
   let newfilter = List.map2 test (evar_context evi) filter in
   if eq_filter newfilter (evar_filter evi) then None else Some newfilter
 
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 76587a340..8269674d7 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -24,8 +24,9 @@ let crazy_type =  mkSet
 
 let decompose_prod env t =
   let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in
-  if name = Anonymous then (Name (Id.of_string "x"),dom,codom)
-  else res
+  match name with
+  | Anonymous -> (Name (Id.of_string "x"), dom, codom)
+  | Name _ -> res
 
 exception Find_at of int
 
@@ -36,7 +37,8 @@ let invert_tag cst tag reloc_tbl =
   try
     for j = 0 to Array.length reloc_tbl - 1 do
       let tagj,arity = reloc_tbl.(j) in
-      if tag = tagj && (cst && arity = 0 || not(cst || arity = 0)) then
+      let no_arity = Int.equal arity 0 in
+      if Int.equal tag tagj && (cst && no_arity || not (cst || no_arity)) then
 	raise (Find_at j)
       else ()
     done;raise Not_found
@@ -57,7 +59,7 @@ let type_constructor mind mib typ params =
   let s = ind_subst mind mib in
   let ctyp = substl s typ in
   let nparams = Array.length params in
-  if nparams = 0 then ctyp
+  if Int.equal nparams 0 then ctyp
   else
     let _,ctyp = decompose_prod_n nparams ctyp in
     substl (Array.rev_to_list params) ctyp
@@ -218,7 +220,7 @@ and nf_predicate env ind mip params v pT =
       let name = Name (Id.of_string "c") in
       let n = mip.mind_nrealargs in
       let rargs = Array.init n (fun i -> mkRel (n-i)) in
-      let params = if n=0 then params else Array.map (lift n) params in
+      let params = if Int.equal n 0 then params else Array.map (lift n) params in
       let dom = mkApp(mkInd ind,Array.append params rargs) in
       let body = nf_vtype (push_rel (name,None,dom) env) vb in
       true, mkLambda(name,dom,body)