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

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

13 files changed, 100 insertions, 54 deletions

diff --git a/dev/ci/user-overlays/10441-ppedrot-static-poly-section.sh b/dev/ci/user-overlays/10441-ppedrot-static-poly-section.sh
new file mode 100644
index 0000000000..00f544f894
--- /dev/null
+++ b/dev/ci/user-overlays/10441-ppedrot-static-poly-section.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10441" ] || [ "$CI_BRANCH" = "static-poly-section" ]; then
+
+    ext_lib_CI_REF=static-poly-section
+    ext_lib_CI_GITURL=https://github.com/ppedrot/coq-ext-lib
+
+fi
diff --git a/doc/changelog/02-specification-language/10441-static-poly-section.rst b/doc/changelog/02-specification-language/10441-static-poly-section.rst
new file mode 100644
index 0000000000..7f0345d946
--- /dev/null
+++ b/doc/changelog/02-specification-language/10441-static-poly-section.rst
@@ -0,0 +1,11 @@
+- The universe polymorphism setting now applies from the opening of a section.
+  In particular, it is not possible anymore to mix polymorphic and monomorphic
+  definitions in a section when there are no variables nor universe constraints
+  defined in this section. This makes the behaviour consistent with the
+  documentation. (`#10441 <https://github.com/coq/coq/pull/10441>`_,
+  by Pierre-Marie Pédrot)
+
+- The :cmd:`Section` vernacular command now accepts the "universes" attribute. In
+  addition to setting the section universe polymorphism, it also locally sets
+  the universe polymorphic option inside the section.
+  (`#10441 <https://github.com/coq/coq/pull/10441>`_, by Pierre-Marie Pédrot)
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 395b5ce2d3..7e698bfb66 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -144,6 +144,8 @@ Many other commands support the ``Polymorphic`` flag, including:
 - ``Lemma``, ``Axiom``, and all the other “definition” keywords support
   polymorphism.
 
+- :cmd:`Section` will locally set the polymorphism flag inside the section.
+
 - ``Variables``, ``Context``, ``Universe`` and ``Constraint`` in a section support
   polymorphism. This means that the universe variables (and associated
   constraints) are discharged polymorphically over definitions that use
diff --git a/library/lib.ml b/library/lib.ml
index d461644d56..59b55cc16b 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -427,46 +427,60 @@ type secentry =
   | Variable of {
       id:Names.Id.t;
       kind:Decl_kinds.binding_kind;
-      poly:bool;
       univs:Univ.ContextSet.t;
     }
   | Context of Univ.ContextSet.t
 
-let sectab =
-  Summary.ref ([] : (secentry list * Opaqueproof.work_list * abstr_list) list)
-    ~name:"section-context"
+type section_data = {
+  sec_entry : secentry list;
+  sec_workl : Opaqueproof.work_list;
+  sec_abstr : abstr_list;
+  sec_poly  : bool;
+}
 
-let add_section () =
-  sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty),
-                (Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab
+let empty_section_data ~poly = {
+  sec_entry = [];
+  sec_workl = (Names.Cmap.empty,Names.Mindmap.empty);
+  sec_abstr = (Names.Cmap.empty,Names.Mindmap.empty);
+  sec_poly  = poly;
+}
 
-let check_same_poly p vars =
-  let pred = function Context _ -> p = false | Variable {poly} -> p != poly in
-  if List.exists pred vars then
+let sectab =
+  Summary.ref ([] : section_data list) ~name:"section-context"
+
+let check_same_poly p sec =
+  if p != sec.sec_poly then
     user_err Pp.(str  "Cannot mix universe polymorphic and monomorphic declarations in sections.")
 
+let add_section ~poly () =
+  List.iter (fun tab -> check_same_poly poly tab) !sectab;
+  sectab := empty_section_data ~poly :: !sectab
+
 let add_section_variable ~name ~kind ~poly univs =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
-    | (vars,repl,abs)::sl ->
-       List.iter (fun tab -> check_same_poly poly (pi1 tab)) !sectab;
-       sectab := (Variable {id=name;kind;poly;univs}::vars,repl,abs)::sl
+    | s :: sl ->
+       List.iter (fun tab -> check_same_poly poly tab) !sectab;
+       let s = { s with sec_entry = Variable {id=name;kind;univs} :: s.sec_entry } in
+       sectab := s :: sl
 
 let add_section_context ctx =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
-    | (vars,repl,abs)::sl ->
-       check_same_poly true vars;
-       sectab := (Context ctx :: vars,repl,abs)::sl
+    | s :: sl ->
+       check_same_poly true s;
+       let s = { s with sec_entry = Context ctx :: s.sec_entry } in
+       sectab := s :: sl
 
 exception PolyFound of bool (* make this a let exception once possible *)
 let is_polymorphic_univ u =
   try
     let open Univ in
-    List.iter (fun (vars,_,_) ->
+    List.iter (fun s ->
+      let vars = s.sec_entry in
         List.iter (function
-            | Variable {poly;univs=(univs,_)} ->
-              if LSet.mem u univs then raise (PolyFound poly)
+            | Variable {univs=(univs,_)} ->
+              if LSet.mem u univs then raise (PolyFound s.sec_poly)
             | Context (univs,_) ->
               if LSet.mem u univs then raise (PolyFound true)
           ) vars
@@ -474,12 +488,12 @@ let is_polymorphic_univ u =
     false
   with PolyFound b -> b
 
-let extract_hyps (secs,ohyps) =
+let extract_hyps poly (secs,ohyps) =
   let rec aux = function
-    | (Variable {id;kind;poly;univs}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
+    | (Variable {id;kind;univs}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
       let l, r = aux (idl,hyps) in 
       (decl,kind) :: l, if poly then Univ.ContextSet.union r univs else r
-    | (Variable {poly;univs}::idl,hyps) ->
+    | (Variable {univs}::idl,hyps) ->
         let l, r = aux (idl,hyps) in
           l, if poly then Univ.ContextSet.union r univs else r
     | (Context ctx :: idl, hyps) ->
@@ -511,9 +525,9 @@ let name_instance inst =
 let add_section_replacement f g poly hyps =
   match !sectab with
   | [] -> ()
-  | (vars,exps,abs)::sl ->
-    let () = check_same_poly poly vars in
-    let sechyps,ctx = extract_hyps (vars,hyps) in
+  | s :: sl ->
+    let () = check_same_poly poly s in
+    let sechyps,ctx = extract_hyps s.sec_poly (s.sec_entry, hyps) in
     let ctx = Univ.ContextSet.to_context ctx in
     let inst = Univ.UContext.instance ctx in
     let nas = name_instance inst in
@@ -524,7 +538,11 @@ let add_section_replacement f g poly hyps =
       abstr_subst = subst;
       abstr_uctx = ctx;
     } in
-    sectab := (vars,f (inst,args) exps, g info abs) :: sl
+    let s = { s with
+      sec_workl = f (inst, args) s.sec_workl;
+      sec_abstr = g info s.sec_abstr;
+    } in
+    sectab := s :: sl
 
 let add_section_kn ~poly kn =
   let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
@@ -534,13 +552,13 @@ let add_section_constant ~poly kn =
   let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
     add_section_replacement f f poly
 
-let replacement_context () = pi2 (List.hd !sectab)
+let replacement_context () = (List.hd !sectab).sec_workl
 
 let section_segment_of_constant con =
-  Names.Cmap.find con (fst (pi3 (List.hd !sectab)))
+  Names.Cmap.find con (fst (List.hd !sectab).sec_abstr)
 
 let section_segment_of_mutual_inductive kn =
-  Names.Mindmap.find kn (snd (pi3 (List.hd !sectab)))
+  Names.Mindmap.find kn (snd (List.hd !sectab).sec_abstr)
 
 let empty_segment = {
   abstr_ctx = [];
@@ -563,20 +581,20 @@ let section_instance = let open GlobRef in function
        | Variable {id=id'} -> Names.Id.equal id id'
        | Context _ -> false
      in
-     if List.exists eq (pi1 (List.hd !sectab))
+     if List.exists eq (List.hd !sectab).sec_entry
      then Univ.Instance.empty, [||]
      else raise Not_found
   | ConstRef con ->
-      Names.Cmap.find con (fst (pi2 (List.hd !sectab)))
+      Names.Cmap.find con (fst (List.hd !sectab).sec_workl)
   | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
-      Names.Mindmap.find kn (snd (pi2 (List.hd !sectab)))
+      Names.Mindmap.find kn (snd (List.hd !sectab).sec_workl)
 
 let is_in_section ref =
   try ignore (section_instance ref); true with Not_found -> false
 
 (*************)
 (* Sections. *)
-let open_section id =
+let open_section ~poly id =
   let opp = !lib_state.path_prefix in
   let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in
   let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in
@@ -587,7 +605,7 @@ let open_section id =
   (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
   Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix));
   lib_state := { !lib_state with path_prefix = prefix };
-  add_section ()
+  add_section ~poly ()
 
 
 (* Restore lib_stk and summaries as before the section opening, and
diff --git a/library/lib.mli b/library/lib.mli
index 01366ddfd0..fe6bf69ec4 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -147,7 +147,7 @@ val library_part :  GlobRef.t -> DirPath.t
 
 (** {6 Sections } *)
 
-val open_section : Id.t -> unit
+val open_section : poly:bool -> Id.t -> unit
 val close_section : unit -> unit
 
 (** {6 We can get and set the state of the operations (used in [States]). } *)
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.
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.
 (*
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 68b7462bde..46ddf214ab 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -963,9 +963,10 @@ let vernac_include l =
 
 (* Sections *)
 
-let vernac_begin_section ({v=id} as lid) =
+let vernac_begin_section ~poly ({v=id} as lid) =
   Dumpglob.dump_definition lid true "sec";
-  Lib.open_section id
+  Lib.open_section ~poly id;
+  set_bool_option_value_gen ~locality:OptLocal ["Universe"; "Polymorphism"] poly
 
 let vernac_end_section {CAst.loc} =
   Dumpglob.dump_reference ?loc
@@ -2396,8 +2397,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with
   (* Gallina extensions *)
   | VernacBeginSection lid ->
     VtNoProof(fun () ->
-        unsupported_attributes atts;
-        vernac_begin_section lid)
+        vernac_begin_section ~poly:(only_polymorphism atts) lid)
   | VernacEndSegment lid ->
     VtNoProof(fun () ->
         unsupported_attributes atts;