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.
---
 library/lib.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'library/lib.ml')

diff --git a/library/lib.ml b/library/lib.ml
index 1c6f82e8a6..991e23eb3a 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -464,8 +464,8 @@ let section_instance = let open GlobRef in function
 
 (*************)
 (* Sections. *)
-let open_section ~poly id =
-  let () = Global.open_section ~poly in
+let open_section id =
+  let () = Global.open_section () in
   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
-- 
cgit v1.2.3