From 710f74901e0fd65ca677555366cae3d00686c9c8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 29 Oct 2020 16:50:09 +0100
Subject: Fine-tuning the sort of the predicate obtained by small inversion.

If the result is in SProp, Prop or (impredicative) Set, we preserve
this information since the elimination sort might be restricted by the
sort of the destructed type.

If the result is in Type, we use a fresh sort upper bound so that we
are sure not having residual algebraic universes which would raise
problems in a type constraint (e.g. in define_evar_as_product).

This fixes the part of #13278 posted on discourse.
---
 test-suite/bugs/closed/bug_13278.v | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_13278.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_13278.v b/test-suite/bugs/closed/bug_13278.v
new file mode 100644
index 0000000000..44a14174cd
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13278.v
@@ -0,0 +1,8 @@
+Inductive even: nat -> Prop :=
+| evenB: even 0
+| evenS: forall n, even n -> even (S (S n)).
+
+Goal even 1 -> False.
+Proof.
+  refine (fun a => match a with end).
+Qed.
-- 
cgit v1.2.3