Fixing pervasives equalities in Vconv.

1 files changed, 16 insertions, 15 deletions

diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 4273596d9..484ee2a50 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -1,3 +1,4 @@
+open Util
 open Names
 open Term
 open Environ
@@ -15,8 +16,8 @@ let val_of_constr env c =
 
 let compare_zipper z1 z2 =
   match z1, z2 with
-  | Zapp args1, Zapp args2 -> nargs args1 = nargs args2
-  | Zfix(f1,args1), Zfix(f2,args2) ->  nargs args1 = nargs args2
+  | Zapp args1, Zapp args2 -> Int.equal (nargs args1) (nargs args2)
+  | Zfix(f1,args1), Zfix(f2,args2) ->  Int.equal (nargs args1) (nargs args2)
   | Zswitch _, Zswitch _ -> true
   | _ , _ -> false
 
@@ -31,7 +32,7 @@ let rec compare_stack stk1 stk2 =
 (* Conversion *)
 let conv_vect fconv vect1 vect2 cu =
   let n = Array.length vect1 in
-  if n = Array.length vect2 then
+  if Int.equal n (Array.length vect2) then
     let rcu = ref cu in
     for i = 0 to n - 1 do
       rcu := fconv vect1.(i) vect2.(i) !rcu
@@ -61,10 +62,10 @@ and conv_whd pb k whd1 whd2 cu =
       if nargs args1 <> nargs args2 then raise NotConvertible
       else conv_arguments k args1 args2 (conv_cofix k cf1 cf2 cu)
   | Vconstr_const i1, Vconstr_const i2 ->
-      if i1 = i2 then cu else raise NotConvertible
+      if Int.equal i1 i2 then cu else raise NotConvertible
   | Vconstr_block b1, Vconstr_block b2 ->
       let sz = bsize b1 in
-      if btag b1 = btag b2 && sz = bsize b2 then
+      if Int.equal (btag b1) (btag b2) && Int.equal sz (bsize b2) then
 	let rcu = ref cu in
 	for i = 0 to sz - 1 do
 	  rcu := conv_val CONV k (bfield b1 i) (bfield b2 i) !rcu
@@ -89,7 +90,7 @@ and conv_atom pb k a1 stk1 a2 stk2 cu =
 	conv_stack k stk1 stk2 cu
       else raise NotConvertible
   | Aid ik1, Aid ik2 ->
-      if ik1 = ik2 && compare_stack stk1 stk2 then
+      if eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
 	conv_stack k stk1 stk2 cu
       else raise NotConvertible
   | Aiddef(ik1,v1), Aiddef(ik2,v2) ->
@@ -160,7 +161,7 @@ and conv_arguments k args1 args2 cu =
   if args1 == args2 then cu
   else
     let n = nargs args1 in
-    if n = nargs args2 then
+    if Int.equal n (nargs args2) then
       let rcu = ref cu in
       for i = 0 to n - 1 do
 	rcu := conv_val CONV k (arg args1 i) (arg args2 i) !rcu
@@ -173,11 +174,11 @@ let rec conv_eq pb t1 t2 cu =
   else
     match kind_of_term t1, kind_of_term t2 with
     | Rel n1, Rel n2 ->
-	if n1 = n2 then cu else raise NotConvertible
+	if Int.equal n1 n2 then cu else raise NotConvertible
     | Meta m1, Meta m2 ->
-	if m1 = m2 then cu else raise NotConvertible
+	if Int.equal m1 m2 then cu else raise NotConvertible
     | Var id1, Var id2 ->
-	if id1 = id2 then cu else raise NotConvertible
+	if Id.equal id1 id2 then cu else raise NotConvertible
     | Sort s1, Sort s2 -> sort_cmp pb s1 s2 cu
     | Cast (c1,_,_), _ -> conv_eq pb c1 t2 cu
     | _, Cast (c2,_,_) -> conv_eq pb t1 c2 cu
@@ -189,7 +190,7 @@ let rec conv_eq pb t1 t2 cu =
     | App (c1,l1), App (c2,l2) ->
 	conv_eq_vect l1 l2 (conv_eq CONV c1 c2 cu)
     | Evar (e1,l1), Evar (e2,l2) ->
-	if e1 = e2 then conv_eq_vect l1 l2 cu
+	if Evar.equal e1 e2 then conv_eq_vect l1 l2 cu
 	else raise NotConvertible
     | Const c1, Const c2 ->
 	if eq_constant c1 c2 then cu else raise NotConvertible
@@ -201,17 +202,17 @@ let rec conv_eq pb t1 t2 cu =
 	let pcu = conv_eq CONV p1 p2 cu in
 	let ccu = conv_eq CONV c1 c2 pcu in
 	conv_eq_vect bl1 bl2 ccu
-    | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
-	if ln1 = ln2 then conv_eq_vect tl1 tl2 (conv_eq_vect bl1 bl2 cu)
+    | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
+	if Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 then conv_eq_vect tl1 tl2 (conv_eq_vect bl1 bl2 cu)
 	else raise NotConvertible
     | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
-	if ln1 = ln2 then conv_eq_vect tl1 tl2 (conv_eq_vect bl1 bl2 cu)
+	if Int.equal ln1 ln2 then conv_eq_vect tl1 tl2 (conv_eq_vect bl1 bl2 cu)
 	else raise NotConvertible
     | _ -> raise NotConvertible
 
 and conv_eq_vect vt1 vt2 cu =
   let len = Array.length vt1 in
-  if len = Array.length vt2 then
+  if Int.equal len (Array.length vt2) then
     let rcu = ref cu in
     for i = 0 to len-1 do
       rcu := conv_eq CONV vt1.(i) vt2.(i) !rcu