diff options
| author | gareuselesinge | 2011-12-12 14:00:45 +0000 |
|---|---|---|
| committer | gareuselesinge | 2011-12-12 14:00:45 +0000 |
| commit | 7e1fefc0a095f7bb7f720218f9d472d4b0d6507d (patch) | |
| tree | a853d983f64e85d752d771df1e8f2044879a6ca2 /proofs/proof_global.ml | |
| 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.ml')
| -rw-r--r-- | proofs/proof_global.ml | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index e9af46ba9b..2745270a65 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -267,6 +267,16 @@ let set_endline_tactic tac = let p = give_me_the_proof () in Proof.set_endline_tactic tac p +let set_used_variables l = + let p = give_me_the_proof () in + let env = Global.env () in + let ids = List.fold_right Idset.add l Idset.empty in + let ctx = Environ.keep_hyps env ids in + Proof.set_used_variables ctx p + +let get_used_variables () = + Proof.get_used_variables (give_me_the_proof ()) + let with_end_tac tac = let p = give_me_the_proof () in Proof.with_end_tac p tac @@ -278,9 +288,11 @@ let close_proof () = let id = get_current_proof_name () in let p = give_me_the_proof () in let proofs_and_types = Proof.return p in + let section_vars = Proof.get_used_variables p in let entries = List.map - (fun (c,t) -> { Entries.const_entry_body = c ; - const_entry_type = Some t; + (fun (c,t) -> { Entries.const_entry_body = c; + const_entry_secctx = section_vars; + const_entry_type = Some t; const_entry_opaque = true }) proofs_and_types in |