From 46cad49197abd858ef430c150e32702c01b2f205 Mon Sep 17 00:00:00 2001 From: msozeau Date: Wed, 2 Apr 2008 15:47:07 +0000 Subject: Add the ability to specify the implicit status of section variables and whether or not to keep them regardless of the actual dependencies (in order to implement the proper discharge behavior for type classes). This means adding an argument to rebuild_function in libobject, giving this information on variables after a section's constants have been discharged (discharge_function is too early). Surface syntax for Variable not added yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10741 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/lib.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/lib.mli') 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 -> -- cgit v1.2.3