From c13a3b61c9b1a714c50bcf0ec371a4effe1ff627 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 27 Jun 2019 15:09:40 +0200
Subject: 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.
---
 vernac/vernacentries.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 68b7462bde..e98a15eecc 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -963,9 +963,9 @@ 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
 
 let vernac_end_section {CAst.loc} =
   Dumpglob.dump_reference ?loc
@@ -2396,8 +2396,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;
-- 
cgit v1.2.3


From b8f77d00c586fd17c8447ab6fc74acf97b5597c4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 12 Jul 2019 16:42:06 +0200
Subject: Polymorphism attribute on section sets the option locally.

This is deemed to be more natural as most of the uses will follow this
structure.
---
 vernac/vernacentries.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e98a15eecc..46ddf214ab 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -965,7 +965,8 @@ let vernac_include l =
 
 let vernac_begin_section ~poly ({v=id} as lid) =
   Dumpglob.dump_definition lid true "sec";
-  Lib.open_section ~poly 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
-- 
cgit v1.2.3