diff options
| author | Pierre-Marie Pédrot | 2019-10-04 17:55:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-04 17:55:25 +0200 |
| commit | a8ab4cc9bfa9d31ac08b0ae3e3f318578ce50e2a (patch) | |
| tree | 2040f56dd268a35db0aecf9d98470f42303237a4 /library/lib.mli | |
| parent | 87c17a6871ef4c21ff86a050297d33738c5a870a (diff) | |
| parent | 994edaf989c0232b5c7de70a2f8ccb46c557da95 (diff) | |
Merge PR #10798: Loosen restrictions on mixing universe mono/polymorphism in sections
Reviewed-by: ppedrot
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 2 |
1 files changed, 1 insertions, 1 deletions
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]). } *) |