diff options
| author | Hugo Herbelin | 2020-05-28 18:17:30 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-29 14:06:14 +0200 |
| commit | 22d0e5cf023ce3fc33a8a5c0dd774847aa06e0b0 (patch) | |
| tree | 546eb29528deac11e7a151ce0752b855705af0ea /pretyping | |
| parent | d75b889948fbfd5600d505ab823a0e6da2195af6 (diff) | |
Fixes #12418 (inference of return clause meets assert false).
This is a quick fix to avoid the anomaly, with a fallback on before
b1b8243b7fc.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 5e3fb9dae3..25353b7c12 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1716,7 +1716,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t = let flags = (default_flags_of TransparentState.full) in match solve_simple_eqn evar_unify flags !!env sigma (None,ev,substl inst ev') with | Success evd -> evdref := evd - | UnifFailure _ -> assert false + | UnifFailure _ -> evdref := add_conv_pb (Reduction.CONV,!!env,substl inst ev',t) sigma end; ev' | _ -> |