aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/vconv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/vconv.ml')
-rw-r--r--kernel/vconv.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 8c7658147..84303fc21 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -116,7 +116,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
conv_stack env k stk1 stk2 cu
else raise NotConvertible
| Aid ik1, Aid ik2 ->
- if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
+ if Vmvalues.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
conv_stack env k stk1 stk2 cu
else raise NotConvertible
| Atype _ , _ | _, Atype _ -> assert false