Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 42 insertions, 42 deletions

diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 7c515735..a35d1d88 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -3,10 +3,10 @@ open Declarations
 open Term
 open Environ
 open Conv_oracle
-open Reduction 
+open Reduction
 open Closure
 open Vm
-open Csymtable 
+open Csymtable
 open Univ
 
 let val_of_constr env c =
@@ -27,7 +27,7 @@ let rec compare_stack stk1 stk2 =
   | z1::stk1, z2::stk2 ->
       if compare_zipper z1 z2 then compare_stack stk1 stk2
       else false
-  | _, _ -> false 
+  | _, _ -> false
 
 (* Conversion *)
 let conv_vect fconv vect1 vect2 cu =
@@ -42,13 +42,13 @@ let conv_vect fconv vect1 vect2 cu =
 
 let infos = ref (create_clos_infos betaiotazeta Environ.empty_env)
 
-let rec conv_val pb k v1 v2 cu = 
-  if v1 == v2 then cu 
+let rec conv_val pb k v1 v2 cu =
+  if v1 == v2 then cu
   else conv_whd pb k (whd_val v1) (whd_val v2) cu
-    
-and conv_whd pb k whd1 whd2 cu =  
+
+and conv_whd pb k whd1 whd2 cu =
   match whd1, whd2 with
-  | Vsort s1, Vsort s2 -> sort_cmp pb s1 s2 cu 
+  | Vsort s1, Vsort s2 -> sort_cmp pb s1 s2 cu
   | Vprod p1, Vprod p2 ->
       let cu = conv_val CONV k (dom p1) (dom p2) cu in
       conv_fun pb k (codom p1) (codom p2) cu
@@ -58,11 +58,11 @@ and conv_whd pb k whd1 whd2 cu =
       if nargs args1 <> nargs args2 then raise NotConvertible
       else conv_arguments k args1 args2 (conv_fix k f1 f2 cu)
   | Vcofix (cf1,_,None), Vcofix (cf2,_,None) -> conv_cofix k cf1 cf2 cu
-  | Vcofix (cf1,_,Some args1), Vcofix (cf2,_,Some args2) ->	
+  | Vcofix (cf1,_,Some args1), Vcofix (cf2,_,Some args2) ->
       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 
+  | Vconstr_const i1, Vconstr_const i2 ->
+      if 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
@@ -72,33 +72,33 @@ and conv_whd pb k whd1 whd2 cu =
 	done;
 	!rcu
       else raise NotConvertible
-  | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) -> 
+  | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) ->
       conv_atom pb k a1 stk1 a2 stk2 cu
-  | _, Vatom_stk(Aiddef(_,v),stk) -> 
+  | _, Vatom_stk(Aiddef(_,v),stk) ->
       conv_whd pb k whd1 (force_whd v stk) cu
-  | Vatom_stk(Aiddef(_,v),stk), _ -> 
+  | Vatom_stk(Aiddef(_,v),stk), _ ->
       conv_whd pb k (force_whd v stk) whd2 cu
   | _, _ -> raise NotConvertible
 
 and conv_atom pb k a1 stk1 a2 stk2 cu =
   match a1, a2 with
   | Aind (kn1,i1), Aind(kn2,i2) ->
-      if mind_equiv_infos !infos (kn1,i1) (kn2,i2) && compare_stack stk1 stk2
+      if eq_ind (kn1,i1) (kn2,i2) && compare_stack stk1 stk2
       then
 	conv_stack k stk1 stk2 cu
       else raise NotConvertible
-  | Aid ik1, Aid ik2 -> 
-      if ik1 = ik2 && compare_stack stk1 stk2 then 
-	conv_stack k stk1 stk2 cu 
+  | Aid ik1, Aid ik2 ->
+      if ik1 = ik2 && compare_stack stk1 stk2 then
+	conv_stack k stk1 stk2 cu
       else raise NotConvertible
   | Aiddef(ik1,v1), Aiddef(ik2,v2) ->
       begin
 	try
-	  if ik1 = ik2 && compare_stack stk1 stk2 then
-	    conv_stack k stk1 stk2 cu 
+	  if eq_table_key ik1 ik2 && compare_stack stk1 stk2 then
+	    conv_stack k stk1 stk2 cu
 	  else raise NotConvertible
 	with NotConvertible ->
-	  if oracle_order ik1 ik2 then             
+	  if oracle_order ik1 ik2 then
             conv_whd pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu
           else conv_whd pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu
       end
@@ -106,15 +106,15 @@ and conv_atom pb k a1 stk1 a2 stk2 cu =
       conv_whd pb k (force_whd v1 stk1) (Vatom_stk(a2,stk2)) cu
   | _, Aiddef(ik2,v2) ->
       conv_whd pb k (Vatom_stk(a1,stk1)) (force_whd v2 stk2) cu
-  | _, _ -> raise NotConvertible 
-	
+  | _, _ -> raise NotConvertible
+
 and conv_stack k stk1 stk2 cu =
   match stk1, stk2 with
   | [], [] -> cu
   | Zapp args1 :: stk1, Zapp args2 :: stk2 ->
-      conv_stack k stk1 stk2 (conv_arguments k args1 args2 cu) 
+      conv_stack k stk1 stk2 (conv_arguments k args1 args2 cu)
   | Zfix(f1,args1) :: stk1, Zfix(f2,args2) :: stk2 ->
-      conv_stack k stk1 stk2 
+      conv_stack k stk1 stk2
 	(conv_arguments k args1 args2 (conv_fix k f1 f2 cu))
   | Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 ->
       if check_switch sw1 sw2 then
@@ -122,7 +122,7 @@ and conv_stack k stk1 stk2 cu =
 	let rcu = ref (conv_val CONV k vt1 vt2 cu) in
 	let b1, b2 = branch_of_switch k sw1, branch_of_switch k sw2 in
 	for i = 0 to Array.length b1 - 1 do
-	  rcu := 
+	  rcu :=
 	    conv_val CONV (k + fst b1.(i)) (snd b1.(i)) (snd b2.(i)) !rcu
 	done;
 	conv_stack k stk1 stk2 !rcu
@@ -136,7 +136,7 @@ and conv_fun pb k f1 f2 cu =
     conv_val pb (k+arity) b1 b2 cu
 
 and conv_fix k f1 f2 cu =
-  if f1 == f2 then cu 
+  if f1 == f2 then cu
   else
     if check_fix f1 f2 then
       let bf1, tf1 = reduce_fix k f1 in
@@ -168,34 +168,34 @@ and conv_arguments k args1 args2 cu =
     else raise NotConvertible
 
 let rec conv_eq pb t1 t2 cu =
-  if t1 == t2 then cu 
+  if t1 == t2 then cu
   else
     match kind_of_term t1, kind_of_term t2 with
-    | Rel n1, Rel n2 -> 
+    | Rel n1, Rel n2 ->
 	if n1 = n2 then cu else raise NotConvertible
     | Meta m1, Meta m2 ->
 	if m1 = m2 then cu else raise NotConvertible
-    | Var id1, Var id2 -> 
+    | Var id1, Var id2 ->
 	if 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
-    | Prod (_,t1,c1), Prod (_,t2,c2) -> 
+    | Prod (_,t1,c1), Prod (_,t2,c2) ->
 	conv_eq pb c1 c2 (conv_eq CONV t1 t2 cu)
     | Lambda (_,t1,c1), Lambda (_,t2,c2) -> conv_eq CONV c1 c2 cu
-    | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> 
+    | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) ->
 	conv_eq pb c1 c2 (conv_eq CONV b1 b2 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
 	else raise NotConvertible
-    | Const c1, Const c2 -> 
-	if c1 = c2 then cu else raise NotConvertible
-    | Ind c1, Ind c2 -> 
-	if c1 = c2 then cu else raise NotConvertible
-    | Construct c1, Construct c2 -> 
-	if c1 = c2 then cu else raise NotConvertible
+    | Const c1, Const c2 ->
+	if eq_constant c1 c2 then cu else raise NotConvertible
+    | Ind c1, Ind c2 ->
+	if eq_ind c1 c2 then cu else raise NotConvertible
+    | Construct c1, Construct c2 ->
+	if eq_constructor c1 c2 then cu else raise NotConvertible
     | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
 	let pcu = conv_eq CONV p1 p2 cu in
 	let ccu = conv_eq CONV c1 c2 pcu in
@@ -203,7 +203,7 @@ let rec conv_eq pb t1 t2 cu =
     | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
 	if 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)) ->	
+    | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
 	if ln1 = ln2 then conv_eq_vect tl1 tl2 (conv_eq_vect bl1 bl2 cu)
 	else raise NotConvertible
     | _ -> raise NotConvertible
@@ -216,7 +216,7 @@ and conv_eq_vect vt1 vt2 cu =
       rcu := conv_eq CONV vt1.(i) vt2.(i) !rcu
     done; !rcu
   else raise NotConvertible
-      
+
 let vconv pb env t1 t2 =
   let cu =
     try conv_eq pb t1 t2 Constraint.empty
@@ -227,7 +227,7 @@ let vconv pb env t1 t2 =
       let cu = conv_val pb (nb_rel env) v1 v2 Constraint.empty in
       cu
   in cu
-    
+
 let _ = Reduction.set_vm_conv vconv
 
 let use_vm = ref false
@@ -236,7 +236,7 @@ let set_use_vm b =
   use_vm := b;
   if b then Reduction.set_default_conv vconv
   else Reduction.set_default_conv Reduction.conv_cmp
-      
+
 let use_vm _ = !use_vm