From 9ea8867a0fa8f2a52df102732fdc1a931c659826 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 30 Sep 2015 22:12:25 +0200 Subject: Proof using: let-in policy, optional auto-clear, forward closure* - "Proof using p*" means: use p and any section var about p. - Simplify the grammar/parser for proof using . - Section variables with a body (let-in) are pulled in automatically since they are safe to be used (add no extra quantification) - automatic clear of "unused" section variables made optional: Set Proof Using Clear Unused. since clearing section hypotheses does not "always work" (e.g. hint databases are not really cleaned) - term_typing: trigger a "suggest proof using" message also for Let theorems. --- kernel/term_typing.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/term_typing.mli') diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 1b54b1ea1..8d92bcc68 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -44,4 +44,4 @@ val build_constant_declaration : constant -> env -> Cooking.result -> constant_body val set_suggest_proof_using : - (constant -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> unit) -> unit + (string -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> string) -> unit -- cgit v1.2.3