Attach the universe polymorphic status to sections.

The previous implementation allowed to dynamically decide whether a section
would be monomorphic or polymorphic at the first definition of a variable
or a constraint. Instead of relying on this delayed decision, we set the
universe polymorphic property directly at the time of the section definition.

5 files changed, 14 insertions, 3 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..88391c7bb1 100644
--- a/test-suite/bugs/closed/bug_4503.v
+++ b/test-suite/bugs/closed/bug_4503.v
@@ -5,6 +5,7 @@ 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}.
@@ -30,6 +31,7 @@ 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}.
diff --git a/test-suite/bugs/closed/bug_4816.v b/test-suite/bugs/closed/bug_4816.v
index 00a523842e..50cb7d280a 100644
--- a/test-suite/bugs/closed/bug_4816.v
+++ b/test-suite/bugs/closed/bug_4816.v
@@ -1,3 +1,4 @@
+#[universes(polymorphic)]
 Section foo.
 Polymorphic Universes A B.
 Fail Constraint A <= B.
@@ -5,12 +6,14 @@ 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}.
   Polymorphic Definition bla := Type@{W}.
+  #[universes(polymorphic)]
   Section Bar.
     Fail Constraint X <= Z.
   End Bar.
@@ -21,8 +24,10 @@ 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}.
   End bar.