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


From f8f915df4a8e3c619a4ccb204ea16afacf983430 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 29 Oct 2020 16:49:25 +0100
Subject: Closes #13278: take into account elimination constraints in small
 inversion.

Ideally, if equations t <= ?x were preserving subtyping that could be
simpler. Currently we need however to put a rigid universe as
constraint on the return predicate so that one branch does not force
the return sort to be lower by unification than what another branch
would have needed.
---
 test-suite/bugs/closed/bug_13278.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_13278.v b/test-suite/bugs/closed/bug_13278.v
index 44a14174cd..9831a4d205 100644
--- a/test-suite/bugs/closed/bug_13278.v
+++ b/test-suite/bugs/closed/bug_13278.v
@@ -6,3 +6,10 @@ Goal even 1 -> False.
 Proof.
   refine (fun a => match a with end).
 Qed.
+
+Goal even 1 -> False.
+Proof.
+  refine (fun a => match a in even n
+                   return match n with 1 => False | _ => True end : Prop
+                   with evenB => I | evenS _ _ => I end).
+Qed.
-- 
cgit v1.2.3