Merge PR #12449: Minimize Prop <= i to i := Set

Reviewed-by: mattam82
Ack-by: Janno
Ack-by: gares

4 files changed, 40 insertions, 4 deletions

diff --git a/test-suite/bugs/closed/bug_12414.v b/test-suite/bugs/closed/bug_12414.v
new file mode 100644
index 0000000000..50b4b86eff
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12414.v
@@ -0,0 +1,13 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+Inductive list {T} : Type := | cons (t : T) : list -> list. (* who needs nil anyway? *)
+Arguments list : clear implicits.
+
+Fixpoint map {A B} (f: A -> B) (l : list A) : list B :=
+  let '(cons t l) := l in cons (f t) (map f l).
+About map@{_ _}.
+(* Two universes, as expected. *)
+
+Definition map_Set@{} {A B : Set} := @map A B.
+
+Definition map_Prop@{} {A B : Prop} := @map A B.
diff --git a/test-suite/bugs/closed/bug_12623.v b/test-suite/bugs/closed/bug_12623.v
new file mode 100644
index 0000000000..9fdcb94e0c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12623.v
@@ -0,0 +1,18 @@
+Set Universe Polymorphism.
+
+Axiom M : Type -> Prop.
+Axiom raise : forall {T}, M T.
+
+Inductive goal : Type :=
+| AHyp : forall {A : Type}, goal.
+
+Definition gtactic@{u u0} := goal@{u} -> M@{u0} (False).
+
+Class Seq (C : Type) :=
+  seq : C -> gtactic.
+Arguments seq {C _} _.
+
+Instance seq_one : Seq@{Set _ _} (gtactic) := fun t2 => fun g => raise.
+
+Definition x1 : gtactic := @seq@{_ _ _} _ _ (fun g : goal => raise).
+Definition x2 : gtactic := @seq@{_ _ _} _ seq_one (fun g : goal => raise).
diff --git a/test-suite/bugs/closed/bug_5197.v b/test-suite/bugs/closed/bug_5197.v
index 0c236e12ad..00b9e9bd9d 100644
--- a/test-suite/bugs/closed/bug_5197.v
+++ b/test-suite/bugs/closed/bug_5197.v
@@ -20,11 +20,11 @@ Definition Typeᶠ : TYPE := {|
   rel := fun _ A => (forall ω : Ω, A ω) -> Type;
                           |}.
 Set Printing Universes.
-Fail Definition Typeᵇ : El Typeᶠ :=
+Definition Typeᵇ : El Typeᶠ :=
   mkPack _ _ (fun w => Type) (fun w A => (forall ω, A ω) -> Type).
 
-Definition Typeᵇ : El Typeᶠ :=
-  mkPack _ (fun _ (A : Ω -> Type) => (forall ω : Ω, A ω) -> _) (fun w => Type) (fun w A => (forall ω, A ω) -> Type).
+(* Definition Typeᵇ : El Typeᶠ := *)
+(*   mkPack _ (fun _ (A : Ω -> Type) => (forall ω : Ω, A ω) -> _) (fun w => Type) (fun w A => (forall ω, A ω) -> Type). *)
 
 (** Bidirectional typechecking helps here *)
 Require Import Program.Tactics.
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 9ab8ace39e..0796b507a1 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -457,5 +457,10 @@ Module ObligationRegression.
   (** Test for a regression encountered when fixing obligations for
       stronger restriction of universe context. *)
   Require Import CMorphisms.
-  Check trans_co_eq_inv_arrow_morphism@{_ _ _ _ _  _ _ _}.
+  Check trans_co_eq_inv_arrow_morphism@{_ _ _ _ _  _ _}.
 End ObligationRegression.
+
+Axiom poly@{i} : forall(A : Type@{i}) (a : A), unit.
+
+Definition nonpoly := @poly True Logic.I.
+Definition check := nonpoly@{}.