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.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.mli')
| -rw-r--r-- | proofs/proof.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli index d80ac79af..12af18f40 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -129,6 +129,9 @@ val get_proof_info : proof -> Store.t val set_proof_info : Store.t -> proof -> unit +(* Sets the section variables assumed by the proof *) +val set_used_variables : Sign.section_context -> proof -> unit +val get_used_variables : proof -> Sign.section_context option (*** Endline tactic ***) |