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.
---
 test-suite/bugs/closed/bug_4503.v | 4 ++--
 test-suite/bugs/closed/bug_4816.v | 8 ++++----
 vernac/vernacentries.ml           | 3 ++-
 3 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/test-suite/bugs/closed/bug_4503.v b/test-suite/bugs/closed/bug_4503.v
index 88391c7bb1..c53d4cabc7 100644
--- a/test-suite/bugs/closed/bug_4503.v
+++ b/test-suite/bugs/closed/bug_4503.v
@@ -10,7 +10,7 @@ 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.
 
 
@@ -34,6 +34,6 @@ Set Printing Universes.
 #[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 50cb7d280a..0bb05e77ce 100644
--- a/test-suite/bugs/closed/bug_4816.v
+++ b/test-suite/bugs/closed/bug_4816.v
@@ -1,7 +1,7 @@
 #[universes(polymorphic)]
 Section foo.
 Polymorphic Universes A B.
-Fail Constraint A <= B.
+Fail Monomorphic Constraint A <= B.
 End foo.
 (* gives an anomaly Universe undefined *)
 
@@ -11,11 +11,11 @@ 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.
 
@@ -29,6 +29,6 @@ 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/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