diff options
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 6c826af63..da8ace048 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -175,7 +175,7 @@ val section_segment_of_mutual_inductive: mutual_inductive -> Sign.named_context val section_instance : global_reference -> identifier array -val add_section_variable : identifier -> unit +val add_section_variable : identifier -> bool -> Term.types option -> unit val add_section_constant : constant -> Sign.named_context -> unit val add_section_kn : kernel_name -> Sign.named_context -> unit val replacement_context : unit -> |