diff options
Diffstat (limited to 'kernel/vconv.ml')
| -rw-r--r-- | kernel/vconv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 2de902c827..1432fb9310 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -95,7 +95,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = (* Pp.(msg_debug (str "conv_atom(" ++ pr_atom a1 ++ str ", " ++ pr_atom a2 ++ str ")")) ; *) match a1, a2 with | Aind ((mi,_i) as ind1) , Aind ind2 -> - if eq_ind ind1 ind2 && compare_stack stk1 stk2 then + if Ind.CanOrd.equal ind1 ind2 && compare_stack stk1 stk2 then let ulen = Univ.AUContext.size (Environ.mind_context env mi) in if ulen = 0 then conv_stack env k stk1 stk2 cu |