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

6 files changed, 40 insertions, 3 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index e67c595bd9..3d507f3583 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -91,6 +91,11 @@ let set_end_tac tac =
   let tac = Proofview.V82.tactic tac in
   Proof_global.set_endline_tactic tac
 
+let set_used_variables l =
+  Proof_global.set_used_variables l
+let get_used_variables () =
+  Proof_global.get_used_variables ()
+
 exception NoSuchGoal
 let _ = Errors.register_handler begin function
   | NoSuchGoal -> Util.error "No such goal."
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 289e8c13c1..7297b975f8 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -154,6 +154,12 @@ val get_all_proof_names : unit -> identifier list
 val set_end_tac : tactic -> unit
 
 (** {6 ... } *)
+(** [set_used_variables l] declares that section variables [l] will be
+    used in the proof *)
+val set_used_variables : identifier list -> unit
+val get_used_variables : unit -> Sign.section_context option
+
+(** {6 ... } *)
 (** [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the
    current focused proof or raises a UserError if no proof is focused or
    if there is no [n]th subgoal *)
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;
diff --git a/proofs/proof.mli b/proofs/proof.mli
index d80ac79af2..12af18f408 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 ***)
 
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
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 2f9f4a549d..ed6a60c71f 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