From 7b2a24d0beee17b61281a5c64fca5cf7388479d3 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 18 Feb 2005 22:17:50 +0000 Subject: Moving centralised discharge into dispatched discharge_function; required to delay some computation from before to after caching time + various simplifications and uniformisations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6748 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/lib.mli | 24 ++++++++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) (limited to 'library/lib.mli') diff --git a/library/lib.mli b/library/lib.mli index 0433897ba..9a4a810ae 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -128,8 +128,7 @@ val library_part : global_reference -> dir_path val open_section : identifier -> object_prefix -val close_section : export:bool -> identifier -> - object_prefix * library_segment * Summary.frozen +val close_section : export:bool -> identifier -> unit (*s Backtracking (undo). *) @@ -157,3 +156,24 @@ val reset_initial : unit -> unit (* XML output hooks *) val set_xml_open_section : (identifier -> unit) -> unit val set_xml_close_section : (identifier -> unit) -> unit + + +(*s Section management for discharge *) + +val section_segment : global_reference -> Sign.named_context +val section_instance : global_reference -> Term.constr array + +val add_section_variable : identifier -> unit +val add_section_constant : constant -> Sign.named_context -> unit +val add_section_kn : kernel_name -> Sign.named_context -> unit +val replacement_context : unit -> + (identifier array Cmap.t * identifier array KNmap.t) + +(*s Discharge: decrease the section level if in the current section *) + +val discharge_kn : kernel_name -> kernel_name +val discharge_con : constant -> constant +val discharge_global : global_reference -> global_reference +val discharge_inductive : inductive -> inductive + + -- cgit v1.2.3