aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/reduction.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-03-11 20:29:16 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-03-28 14:16:52 +0200
commit0ade32f84b28d2190360ec79520788142755b5b7 (patch)
tree46b2d11c817707c3b84653b490de3b0aaad42038 /checker/reduction.ml
parentbd8606189268c3fcdd3506872d459cb9032a33bf (diff)
[api] Deprecate a couple of aliases that we missed.
Diffstat (limited to 'checker/reduction.ml')
-rw-r--r--checker/reduction.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 97255dd49..072dec63f 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -54,7 +54,7 @@ let compare_stack_shape stk1 stk2 =
type lft_constr_stack_elt =
Zlapp of (lift * fconstr) array
- | Zlproj of Names.projection * lift
+ | Zlproj of Names.Projection.t * lift
| Zlfix of (lift * fconstr) * lft_constr_stack
| Zlcase of case_info * lift * fconstr * fconstr array
and lft_constr_stack = lft_constr_stack_elt list
@@ -142,7 +142,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
| (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
f fx1 fx2; cmp_rec a1 a2
| (Zlproj (c1,l1),Zlproj (c2,l2)) ->
- if not (Names.eq_con_chk
+ if not (Names.Constant.UserOrd.equal
(Names.Projection.constant c1)
(Names.Projection.constant c2)) then
raise NotConvertible