Merge PR #10441: Attach the universe polymorphic status to sections.

Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Ack-by: mattam82

5 files changed, 20 insertions, 9 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_020.v b/test-suite/bugs/closed/HoTT_coq_020.v
index 73da464bbe..babd180209 100644
--- a/test-suite/bugs/closed/HoTT_coq_020.v
+++ b/test-suite/bugs/closed/HoTT_coq_020.v
@@ -26,6 +26,7 @@ Ltac present_obj from to :=
            | [ |- context[from ?obj ?C] ] => progress change (from obj C) with (to obj C) in *
          end.
 
+#[universes(polymorphic)]
 Section NaturalTransformationComposition.
   Set Universe Polymorphism.
   Context `(C : @Category objC).
@@ -58,6 +59,7 @@ Polymorphic Definition Cat0 : Category Empty_set
 Polymorphic Definition FunctorFrom0 objC (C : Category objC) : Functor Cat0 C
   := Build_Functor Cat0 C (fun x => match x with end).
 
+#[universes(polymorphic)]
 Section Law0.
   Polymorphic Variable objC : Type.
   Polymorphic Variable C : Category objC.
diff --git a/test-suite/bugs/closed/HoTT_coq_098.v b/test-suite/bugs/closed/HoTT_coq_098.v
index bdcd8ba97d..3b58605575 100644
--- a/test-suite/bugs/closed/HoTT_coq_098.v
+++ b/test-suite/bugs/closed/HoTT_coq_098.v
@@ -21,6 +21,7 @@ Polymorphic Definition GraphIndexingCategory : @SpecializedCategory GraphIndex.
 Admitted.
 
 Module success.
+  #[universes(polymorphic)]
   Section SpecializedFunctor.
     Set Universe Polymorphism.
     Context `(C : @SpecializedCategory objC).
@@ -39,6 +40,7 @@ Module success.
 End success.
 
 Module success2.
+  #[universes(polymorphic)]
   Section SpecializedFunctor.
     Polymorphic Context `(C : @SpecializedCategory objC).
     Polymorphic Context `(D : @SpecializedCategory objD).
diff --git a/test-suite/bugs/closed/bug_3314.v b/test-suite/bugs/closed/bug_3314.v
index a5782298c3..794de93b37 100644
--- a/test-suite/bugs/closed/bug_3314.v
+++ b/test-suite/bugs/closed/bug_3314.v
@@ -24,10 +24,10 @@ Fail Eval compute in Lift nat : Prop.
 (*      = nat
      : Prop *)
 
-Section Hurkens.
+Monomorphic Definition Type2 := Type.
+Monomorphic Definition Type1 := Type : Type2.
 
-  Monomorphic Definition Type2 := Type.
-  Monomorphic Definition Type1 := Type : Type2.
+Section Hurkens.
 
   (** Assumption of a retract from Type into Prop *)
 
diff --git a/test-suite/bugs/closed/bug_4503.v b/test-suite/bugs/closed/bug_4503.v
index 26731e3292..c53d4cabc7 100644
--- a/test-suite/bugs/closed/bug_4503.v
+++ b/test-suite/bugs/closed/bug_4503.v
@@ -5,11 +5,12 @@ Class PreOrder (A : Type) (r : A -> A -> Type) : Type :=
 
 (* FAILURE 1 *)
 
+#[universes(polymorphic)]
 Section foo.
   Polymorphic Universes A.
   Polymorphic Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}.
 
-  Fail Definition foo := PO.
+  Fail Monomorphic Definition foo := PO.
 End foo.
 
 
@@ -30,8 +31,9 @@ End ILogic.
 Set Printing Universes.
 
 (* There is still a problem if the class is universe polymorphic *)
+#[universes(polymorphic)]
 Section Embed_ILogic_Pre.
   Polymorphic Universes A T.
-  Fail Context {A : Type@{A}} {ILA: ILogic.ILogic@{A} A}.
+  Fail Monomorphic Context {A : Type@{A}} {ILA: ILogic.ILogic@{A} A}.
 
 End Embed_ILogic_Pre.
diff --git a/test-suite/bugs/closed/bug_4816.v b/test-suite/bugs/closed/bug_4816.v
index 00a523842e..0bb05e77ce 100644
--- a/test-suite/bugs/closed/bug_4816.v
+++ b/test-suite/bugs/closed/bug_4816.v
@@ -1,18 +1,21 @@
+#[universes(polymorphic)]
 Section foo.
 Polymorphic Universes A B.
-Fail Constraint A <= B.
+Fail Monomorphic Constraint A <= B.
 End foo.
 (* gives an anomaly Universe undefined *)
 
 Universes X Y.
+#[universes(polymorphic)]
 Section Foo.
   Polymorphic Universes Z W.
   Polymorphic Constraint W < Z.
 
-  Fail Definition bla := Type@{W}.
+  Fail Monomorphic Definition bla := Type@{W}.
   Polymorphic Definition bla := Type@{W}.
+  #[universes(polymorphic)]
   Section Bar.
-    Fail Constraint X <= Z.
+    Fail Monomorphic Constraint X <= Z.
   End Bar.
 End Foo.
 
@@ -21,9 +24,11 @@ Require Coq.Classes.RelationClasses.
 Class PreOrder (A : Type) (r : A -> A -> Type) : Type :=
 { refl : forall x, r x x }.
 
+#[universes(polymorphic)]
 Section qux.
   Polymorphic Universes A.
+  #[universes(polymorphic)]
   Section bar.
-    Fail Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}.
+    Fail Monomorphic Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}.
   End bar.
 End qux.