diff options
| author | Emilio Jesus Gallego Arias | 2020-06-01 16:36:44 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-01 16:36:44 +0200 |
| commit | 558e20c25d2e030d4ba4a0b42458969564815223 (patch) | |
| tree | 233d672aa44ea749f96cea01c414c736d6db403a /pretyping | |
| parent | 4270ed35f2a26f226b01f2293f61d18773e6260b (diff) | |
| parent | dec5edf7c92950881693afe2040d711155cf15b5 (diff) | |
Merge PR #12422: Fixes #12418: an assert false in inference of return clause
Reviewed-by: gares
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' | _ -> |