diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-07-07 17:31:04 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-07-07 17:33:27 +0200 |
| commit | 3264fdaa71b2327a992286a08df0dfbcf78ea4fe (patch) | |
| tree | 2cfcdfd2eb96d82a66a03df38954fd7ff8767684 /checker/reduction.ml | |
| parent | 7c7726a798caa6b506a727703de24d2bb5bb3956 (diff) | |
Checker: Fix bug #4282
Adapt to new [projection] abstract type comprising a constant and
a boolean.
Diffstat (limited to 'checker/reduction.ml')
| -rw-r--r-- | checker/reduction.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/checker/reduction.ml b/checker/reduction.ml index 28fdb130e..58f0f894f 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -52,7 +52,7 @@ let compare_stack_shape stk1 stk2 = type lft_constr_stack_elt = Zlapp of (lift * fconstr) array - | Zlproj of Names.constant * lift + | Zlproj of Names.projection * 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 @@ -137,7 +137,9 @@ 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 c1 c2) then + if not (Names.eq_con_chk + (Names.Projection.constant c1) + (Names.Projection.constant c2)) then raise NotConvertible | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) -> if not (fmind ci1.ci_ind ci2.ci_ind) then |