diff options
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/library/lib.mli b/library/lib.mli index fa3bd3f48..787dc969e 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -186,4 +186,9 @@ val discharge_con : Names.constant -> Names.constant val discharge_global : Globnames.global_reference -> Globnames.global_reference val discharge_inductive : Names.inductive -> Names.inductive +(* discharging a constant in one go *) +val full_replacement_context : unit -> Lazyconstr.work_list list +val full_section_segment_of_constant : + Names.constant -> (Context.named_context -> Context.named_context) list + |