Merge PR #10798: Loosen restrictions on mixing universe mono/polymorphism in sections

Reviewed-by: ppedrot

4 files changed, 5 insertions, 5 deletions

diff --git a/library/global.ml b/library/global.ml
index 315a147d2c..c4685370d1 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -109,7 +109,7 @@ let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
 let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl)
 let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl)
 
-let open_section ~poly = globalize0 (Safe_typing.open_section ~poly)
+let open_section () = globalize0 Safe_typing.open_section
 let close_section fs = globalize0_with_summary fs Safe_typing.close_section
 
 let start_module id = globalize (Safe_typing.start_module (i2l id))
diff --git a/library/global.mli b/library/global.mli
index 26ccb90271..c45bf65d84 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -73,7 +73,7 @@ val add_include :
 
 (** Sections *)
 
-val open_section : poly:bool -> unit
+val open_section : unit -> unit
 (** [poly] is true when the section should be universe polymorphic *)
 
 val close_section : Summary.frozen -> unit
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
diff --git a/library/lib.mli b/library/lib.mli
index 5ce601f2d3..d3315b0f2e 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -147,7 +147,7 @@ val library_part :  GlobRef.t -> DirPath.t
 
 (** {6 Sections } *)
 
-val open_section : poly:bool -> Id.t -> unit
+val open_section : Id.t -> unit
 val close_section : unit -> unit
 
 (** {6 We can get and set the state of the operations (used in [States]). } *)