diff options
| author | Pierre-Marie Pédrot | 2020-09-22 14:19:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-21 12:20:10 +0200 |
| commit | 0590764209dcb8540b5292aca38fe2df38b90ab9 (patch) | |
| tree | cede5a6e0a7fabcfd55f7635604493876821afc6 /kernel/reduction.ml | |
| parent | 2b91a8989687e152f7120aa6c907ffeba8495bab (diff) | |
Same little game with Projection.
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index f295b36b60..8eb1c10f70 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -441,7 +441,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | Some s2 -> eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv | None -> - if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2) + if Projection.Repr.CanOrd.equal (Projection.repr p1) (Projection.repr p2) && compare_stack_shape v1 v2 then let el1 = el_stack lft1 v1 in let el2 = el_stack lft2 v2 in @@ -704,7 +704,7 @@ and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv = | (Zlapp a1,Zlapp a2) -> Array.fold_right2 f a1 a2 cu1 | (Zlproj (c1,_l1),Zlproj (c2,_l2)) -> - if not (Projection.Repr.equal c1 c2) then + if not (Projection.Repr.CanOrd.equal c1 c2) then raise NotConvertible else cu1 | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> |