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, 14 insertions, 1 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 110e6190c..435d85233 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -674,6 +674,15 @@ let vernac_set_end_tac tac =
   if tac <> (Tacexpr.TacId []) then set_end_tac (Tacinterp.interp tac) else ()
     (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
 
+let vernac_set_used_variables l =
+  let l = List.map snd l in
+  if not (list_distinct l) then error "Used variables list contains duplicates";
+  let vars = Environ.named_context (Global.env ()) in
+  List.iter (fun id -> 
+    if not (List.exists (fun (id',_,_) -> id = id') vars) then
+      error ("Unknown variable: " ^ string_of_id id))
+    l;
+  set_used_variables l
 
 (*****************************)
 (* Auxiliary file management *)
@@ -1514,7 +1523,11 @@ let interp c = match c with
   | VernacEndSubproof -> vernac_end_subproof ()
   | VernacShow s -> vernac_show s
   | VernacCheckGuard -> vernac_check_guard ()
-  | VernacProof tac -> vernac_set_end_tac tac
+  | VernacProof (None, None) -> ()
+  | VernacProof (Some tac, None) -> vernac_set_end_tac tac
+  | VernacProof (None, Some l) -> vernac_set_used_variables l
+  | VernacProof (Some tac, Some l) -> 
+      vernac_set_end_tac tac; vernac_set_used_variables l
   | VernacProofMode mn -> Proof_global.set_proof_mode mn
   (* Toplevel control *)
   | VernacToplevelControl e -> raise e