diff options
| author | Gaëtan Gilbert | 2019-07-22 13:02:02 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-22 13:02:02 +0200 |
| commit | 033021860b2ea6fee901f6c760dcd8292ed07fe5 (patch) | |
| tree | e775cbf222039ca80878924529ac21b12fbe66fd /library/lib.mli | |
| parent | 21b6ba98b0c0e33ceb106fd164def38d87ff3f0c (diff) | |
| parent | eabe207bc6159f1349f7e6b8e63a55984ea9aa32 (diff) | |
Merge PR #10441: Attach the universe polymorphic status to sections.
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Ack-by: mattam82
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 01366ddfd0..fe6bf69ec4 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 : Id.t -> unit +val open_section : poly:bool -> Id.t -> unit val close_section : unit -> unit (** {6 We can get and set the state of the operations (used in [States]). } *) |