Removing a bunch of generic equalities.

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

7 files changed, 20 insertions, 13 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index f751343bc..f2d66f03a 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -365,6 +365,9 @@ let rec eq_constr m n =
 
 let equal m n = eq_constr m n (* to avoid tracing a recursive fun *)
 
+(** We only use this function over blocks! *)
+let tag t = Obj.tag (Obj.repr t)
+
 let constr_ord_int f t1 t2 =
   let (=?) f g i1 i2 j1 j2=
     let c = f i1 i2 in
@@ -403,7 +406,7 @@ let constr_ord_int f t1 t2 =
     | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
         ((Int.compare =? (Array.compare f)) ==? (Array.compare f))
         ln1 ln2 tl1 tl2 bl1 bl2
-    | t1, t2 -> Pervasives.compare t1 t2
+    | t1, t2 -> Int.compare (tag t1) (tag t2)
 
 let rec compare m n=
   constr_ord_int compare m n
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 9f981f482..973859ede 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -266,3 +266,4 @@ let union_side_effects l1 l2 = l1 @ l2
 let flatten_side_effects l = List.flatten l
 let side_effects_of_list l = l
 let cons_side_effects x l = x :: l
+let side_effects_is_empty = List.is_empty
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 54eed5ea6..f593b4547 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -40,6 +40,7 @@ val union_side_effects : side_effects -> side_effects -> side_effects
 val flatten_side_effects : side_effects list -> side_effects
 val side_effects_of_list : side_effect list -> side_effects
 val cons_side_effects : side_effect -> side_effects -> side_effects
+val side_effects_is_empty : side_effects -> bool
 
 (** {6 Inductive types} *)
 
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 9d069d4e6..fbee52dd7 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -135,8 +135,8 @@ let dummy_symb = SymbValue (dummy_value ())
 
 let eq_symbol sy1 sy2 =
   match sy1, sy2 with
-  | SymbValue v1, SymbValue v2 -> v1 = v2
-  | SymbSort s1, SymbSort s2 -> Int.equal (sorts_ord s1 s2) 0
+  | SymbValue v1, SymbValue v2 -> Pervasives.(=) v1 v2 (** FIXME: how is this even valid? *)
+  | SymbSort s1, SymbSort s2 -> Sorts.equal s1 s2
   | SymbName n1, SymbName n2 -> Name.equal n1 n2
   | SymbConst kn1, SymbConst kn2 -> Constant.equal kn1 kn2
   | SymbMatch sw1, SymbMatch sw2 -> eq_annot_sw sw1 sw2
@@ -349,7 +349,7 @@ and eq_mllam_branches gn1 gn2 n env1 env2 br1 br2 =
 let rec hash_mllambda gn n env t =
   match t with
   | MLlocal ln -> combinesmall 1 (LNmap.find ln env)
-  | MLglobal gn' -> combinesmall 2 (if gn = gn' then 0 else Hashtbl.hash gn')
+  | MLglobal gn' -> combinesmall 2 (if eq_gname gn gn' then 0 else Hashtbl.hash gn')
   | MLprimitive prim -> combinesmall 3 (Hashtbl.hash prim)
   | MLlam (lns, ml) ->
       let env = push_lnames n env lns in
@@ -513,9 +513,10 @@ let eq_global g1 g2 =
       let t1 = MLmatch (annot1,c1,accu1,br1) in
       let t2 = MLmatch (annot2,c2,accu2,br2) in
       eq_mllambda gn1 gn2 (Array.length lns1) env1 env2 t1 t2
-  | Gopen s1, Gopen s2 -> s1 = s2
-  | Gtype (ind1, arr1), Gtype (ind2, arr2) -> ind1 = ind2 && arr1 = arr2
-  | Gcomment s1, Gcomment s2 -> s1 = s2
+  | Gopen s1, Gopen s2 -> String.equal s1 s2
+  | Gtype (ind1, arr1), Gtype (ind2, arr2) ->
+      eq_ind ind1 ind2 && Array.equal Int.equal arr1 arr2
+  | Gcomment s1, Gcomment s2 -> String.equal s1 s2
   | _, _ -> false
 
 let hash_global g =
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index f03d4f799..c38b72031 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -140,7 +140,7 @@ let args_of_accu (k:accumulator) =
 
 let is_accu x =
   let o = Obj.repr x in
-  Obj.is_block o && Obj.tag o = accumulate_tag
+  Obj.is_block o && Int.equal (Obj.tag o) accumulate_tag
 
 (*let accumulate_fix_code (k:accumulator) (a:t) =
   match atom_of_accu k with
@@ -236,7 +236,7 @@ let kind_of_value (v:t) =
   if Obj.is_int o then Vconst (Obj.magic v)
   else
     let tag = Obj.tag o in
-    if tag = accumulate_tag then 
+    if Int.equal tag accumulate_tag then
       Vaccu (Obj.magic v)
     else 
       if (tag < Obj.lazy_tag) then Vblock (Obj.magic v)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index ef0270e9d..567511c93 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -54,7 +54,7 @@ let handle_side_effects env body side_eff =
     let cname c = 
       let name = string_of_con c in
       for i = 0 to String.length name - 1 do
-        if name.[i] = '.' || name.[i] = '#' then name.[i] <- '_' done;
+        if name.[i] == '.' || name.[i] == '#' then name.[i] <- '_' done;
       Name (id_of_string name) in
     let rec sub c i x = match kind_of_term x with
       | Const c' when eq_constant c c' -> mkRel i
@@ -83,7 +83,7 @@ let infer_declaration ?(what="UNKNOWN") env dcl =
   match dcl with
   | DefinitionEntry c ->
       let ctx, entry_body = c.const_entry_secctx, c.const_entry_body in
-      if c.const_entry_opaque && c.const_entry_type <> None then
+      if c.const_entry_opaque && not (Option.is_empty c.const_entry_type) then
         let id = "infer_declaration " ^ what in
         let body_cst =
           Future.chain ~id entry_body (fun (body, side_eff) ->
@@ -138,7 +138,7 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
   (* We try to postpone the computation of used section variables *)
   let hyps, def = 
     match ctx with
-    | None when named_context env <> [] -> 
+    | None when not (List.is_empty (named_context env)) -> 
         (* No declared section vars, and non-empty section context:
            we must look at the body NOW, if any *)
         let ids_typ = global_vars_set_constant_type env typ in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index ce9d9c419..d56904bae 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -712,6 +712,7 @@ let check_sorted g sorted =
     - a [le] edge is initially added from [bottom] to all other
       vertices, and [bottom] is used as the source vertex
 *)
+
 let bellman_ford bottom g =
   let () = match lookup_level bottom g with
   | None -> ()
@@ -720,7 +721,7 @@ let bellman_ford bottom g =
   let ( << ) a b = match a, b with
     | _, None -> true
     | None, _ -> false
-    | Some x, Some y -> x < y
+    | Some x, Some y -> (x : int) < y
   and ( ++ ) a y = match a with
     | None -> None
     | Some x -> Some (x-y)