aboutsummaryrefslogtreecommitdiff
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 4e4168922d..d19bea5199 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -139,7 +139,7 @@ and conv_stack env k stk1 stk2 cu =
conv_stack env k stk1 stk2 !rcu
else raise NotConvertible
| Zproj p1 :: stk1, Zproj p2 :: stk2 ->
- if Constant.equal p1 p2 then conv_stack env k stk1 stk2 cu
+ if Projection.Repr.equal p1 p2 then conv_stack env k stk1 stk2 cu
else raise NotConvertible
| [], _ | Zapp _ :: _, _ | Zfix _ :: _, _ | Zswitch _ :: _, _
| Zproj _ :: _, _ -> raise NotConvertible