From 22d0e5cf023ce3fc33a8a5c0dd774847aa06e0b0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 28 May 2020 18:17:30 +0200
Subject: Fixes #12418 (inference of return clause meets assert false).

This is a quick fix to avoid the anomaly, with a fallback on before
b1b8243b7fc.
---
 pretyping/cases.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

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'
     | _ ->
-- 
cgit v1.2.3