aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/vconv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/vconv.ml')
-rw-r--r--kernel/vconv.ml11
1 files changed, 6 insertions, 5 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 3f9345ff8..80b15f8ba 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -86,23 +86,24 @@ and conv_whd env pb k whd1 whd2 cu =
and conv_atom env pb k a1 stk1 a2 stk2 cu =
match a1, a2 with
- | Aind (kn1,i1), Aind(kn2,i2) ->
- if eq_ind (kn1,i1) (kn2,i2) && compare_stack stk1 stk2
+ | Aind ind1, Aind ind2 ->
+ if eq_puniverses eq_ind ind1 ind2 && compare_stack stk1 stk2
then
conv_stack env k stk1 stk2 cu
else raise NotConvertible
| Aid ik1, Aid ik2 ->
- if eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
+ if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
conv_stack env k stk1 stk2 cu
else raise NotConvertible
| Aiddef(ik1,v1), Aiddef(ik2,v2) ->
begin
try
- if eq_table_key ik1 ik2 && compare_stack stk1 stk2 then
+ if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
conv_stack env k stk1 stk2 cu
else raise NotConvertible
with NotConvertible ->
- if oracle_order (oracle_of_infos !infos) false ik1 ik2 then
+ if oracle_order Univ.out_punivs (oracle_of_infos !infos)
+ false ik1 ik2 then
conv_whd env pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu
else conv_whd env pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu
end