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

1 files changed, 8 insertions, 1 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 2aa31cd253..72730495d7 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -119,6 +119,7 @@ type proof_state = {
 
 type proof_info = {
   mutable endline_tactic : unit Proofview.tactic ;
+  mutable section_vars : Sign.section_context option;
   initial_conclusions : Term.types list
 }
 
@@ -219,6 +220,11 @@ let _unfocus pr =
   pr.state <- { pr.state with proofview = Proofview.unfocus fc pr.state.proofview }
 
 
+let set_used_variables l p =
+  p.info.section_vars <- Some l
+
+let get_used_variables p = p.info.section_vars
+
 (*** Endline tactic ***)
 
 (* spiwack this is an information about the UI, it might be a good idea to move
@@ -364,7 +370,8 @@ let start goals =
       undo_stack = [] ;
       transactions = [] ;
       info = { endline_tactic = Proofview.tclUNIT ();
-	       initial_conclusions = List.map snd goals }
+               initial_conclusions = List.map snd goals;
+               section_vars = None }
     }
   in
   _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr;