diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-12 14:00:45 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-12 14:00:45 +0000 |
| commit | 7e1fefc0a095f7bb7f720218f9d472d4b0d6507d (patch) | |
| tree | a853d983f64e85d752d771df1e8f2044879a6ca2 /proofs/proof_global.mli | |
| parent | dc8f9bb9033702dc7552450c5a3891fd060ee001 (diff) | |
Proof using ...
New vernacular "Proof using idlist" to declare the variables
to be discharged at the end of the current proof. The system
checks that the set of declared variables is a superset of
the set of actually used variables.
It can be combined in a single line with "Proof with":
Proof with .. using ..
Proof using .. with ..
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14789 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/proof_global.mli')
| -rw-r--r-- | proofs/proof_global.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 2f9f4a549..ed6a60c71 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -82,6 +82,10 @@ val run_tactic : unit Proofview.tactic -> unit (** Sets the tactic to be used when a tactic line is closed with [...] *) val set_endline_tactic : unit Proofview.tactic -> unit +(** Sets the section variables assumed by the proof *) +val set_used_variables : Names.identifier list -> unit +val get_used_variables : unit -> Sign.section_context option + (** Appends the endline tactic of the current proof to a tactic. *) val with_end_tac : unit Proofview.tactic -> unit Proofview.tactic |