diff options
| author | Gaëtan Gilbert | 2019-09-27 17:26:26 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-02 14:38:48 +0200 |
| commit | 994edaf989c0232b5c7de70a2f8ccb46c557da95 (patch) | |
| tree | 46f5633c8e3e351a232836f951b8946f71dcf256 /library | |
| parent | 77fd11a9f012a2878e13451e9d8a9f500c6392eb (diff) | |
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.
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 2 | ||||
| -rw-r--r-- | library/global.mli | 2 | ||||
| -rw-r--r-- | library/lib.ml | 4 | ||||
| -rw-r--r-- | library/lib.mli | 2 |
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]). } *) |