diff options
Diffstat (limited to 'toplevel/discharge.mli')
| -rw-r--r-- | toplevel/discharge.mli | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli index b8db027ba..c8af4d1da 100644 --- a/toplevel/discharge.mli +++ b/toplevel/discharge.mli @@ -8,11 +8,10 @@ (*i $Id$ i*) -open Names +open Sign +open Cooking +open Declarations +open Entries -(* This module implements the discharge mechanism. It provides a function to - close the last opened section. That function calls [Lib.close_section] and - then re-introduce all the discharged versions of the objects that were - defined in the section. *) - -val close_section : bool -> identifier -> unit +val process_inductive : + named_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry |