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.

7 files changed, 18 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..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.
diff --git a/test-suite/success/namedunivs.v b/test-suite/success/namedunivs.v
index f9154ef576..01a2136652 100644
--- a/test-suite/success/namedunivs.v
+++ b/test-suite/success/namedunivs.v
@@ -6,6 +6,7 @@
 
 Unset Strict Universe Declaration.
 
+#[universes(polymorphic)]
 Section lift_strict.
 Polymorphic Definition liftlt := 
   let t := Type@{i} : Type@{k} in
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 339f798240..9ab8ace39e 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -122,8 +122,6 @@ Fail Definition id1impred := ((forall A : Type1, A) : Type1).
 
 End Hierarchy.
 
-Section structures.
-
 Record hypo : Type := mkhypo {
    hypo_type : Type;
    hypo_proof : hypo_type
@@ -154,9 +152,6 @@ Polymorphic Definition nest (d : dyn) := {| dyn_proof := d |}.
 
 Polymorphic Definition twoprojs (d : dyn) := dyn_proof d = dyn_proof d.
 
-End structures.
-
-
 Module binders.
 
   Definition mynat@{|} := nat.
@@ -201,7 +196,8 @@ Module binders.
   Definition with_mono@{u|u < M} : Type@{M} := Type@{u}.
 
 End binders.
-    
+
+#[universes(polymorphic)]
 Section cats.
   Local Set Universe Polymorphism.
   Require Import Utf8.
@@ -307,6 +303,7 @@ Fail Check (let A := Set in fooS (id A)).
 Fail Check (let A := Prop in fooS (id A)).
 
 (* Some tests of sort-polymorphisme *)
+#[universes(polymorphic)]
 Section S.
 Polymorphic Variable A:Type.
 (*