diff options
| author | Pierre-Marie Pédrot | 2020-03-31 12:56:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-31 12:56:34 +0200 |
| commit | d03529ab8fec0cad5705b5f775e43ef26c0dedcb (patch) | |
| tree | 65bd33deead3007350bbd93a662ff88017024a99 /kernel | |
| parent | 35b4841eccc645146b62e99edb939fcf4bfcc76d (diff) | |
| parent | 60ec0e0a67e60c52af7e7ef34a2826ef7fb61a26 (diff) | |
Merge PR #11684: Remove spurious anomalies in kernel reduction
Reviewed-by: ppedrot
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/reduction.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 469d5ccaa2..7574d7b21e 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -354,7 +354,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (match kind a1, kind a2 with | (Sort s1, Sort s2) -> if not (is_empty_stack v1 && is_empty_stack v2) then - anomaly (Pp.str "conversion was given ill-typed terms (Sort)."); + (* May happen because we convert application right to left *) + raise NotConvertible; sort_cmp_universes (info_env infos.cnv_inf) cv_pb s1 s2 cuniv | (Meta n, Meta m) -> if Int.equal n m @@ -471,7 +472,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (FProd (x1, c1, c2, e), FProd (_, c'1, c'2, e')) -> if not (is_empty_stack v1 && is_empty_stack v2) then - anomaly (Pp.str "conversion was given ill-typed terms (FProd)."); + (* May happen because we convert application right to left *) + raise NotConvertible; (* Luo's system *) let el1 = el_stack lft1 v1 in let el2 = el_stack lft2 v2 in |