diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-09-30 22:12:25 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-10-08 09:51:13 +0200 |
| commit | 9ea8867a0fa8f2a52df102732fdc1a931c659826 (patch) | |
| tree | 3c3bec0c3ab2459f170ed7270903d47717d4d627 /proofs/proof_global.mli | |
| parent | 0f706b470c83a957b600496c2bca652c2cfe65e3 (diff) | |
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 <expression>.
- 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.
Diffstat (limited to 'proofs/proof_global.mli')
| -rw-r--r-- | proofs/proof_global.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index b5dd5ef85..028116049 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -129,8 +129,10 @@ val set_interp_tac : -> unit (** Sets the section variables assumed by the proof, returns its closure - * (w.r.t. type dependencies *) -val set_used_variables : Names.Id.t list -> Context.section_context + * (w.r.t. type dependencies and let-ins covered by it) + a list of + * ids to be cleared *) +val set_used_variables : + Names.Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list val get_used_variables : unit -> Context.section_context option (**********************************************************) |