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

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

1 files changed, 4 insertions, 4 deletions

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;