From 994edaf989c0232b5c7de70a2f8ccb46c557da95 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 27 Sep 2019 17:26:26 +0200
Subject: Loosen restrictions on mixing universe mono/polymorphism in sections

We disallow adding univ constraints wich refer to polymorphic
universes, and monomorphic constants and inductives when polymorphic
universes or constraints are present.

Every other combination is already correctly discharged by the kernel.
---
 vernac/vernacentries.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 43b58d6d4b..c3be57eec8 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -980,7 +980,9 @@ 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 id;
+  (* If there was no polymorphism attribute this just sets the option
+     to its current value ie noop. *)
   set_bool_option_value_gen ~locality:OptLocal ["Universe"; "Polymorphism"] poly
 
 let vernac_end_section {CAst.loc} =
-- 
cgit v1.2.3