Ajout du vernac Proof with

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3425 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 23 insertions, 3 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 6f682f1133..b8a61e0ecd 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -33,6 +33,7 @@ open Safe_typing
 (*********************************************************************)
 
 type proof_topstate = {
+  mutable top_end_tac : tactic option;
   top_hyps : named_context * named_context;
   top_goal : goal;
   top_strength : Decl_kinds.goal_kind;
@@ -69,6 +70,8 @@ let get_state () =
 let get_topstate ()    = snd(get_state())
 let get_pftreestate () = fst(get_state())
 
+let get_end_tac () = let ts = get_topstate () in ts.top_end_tac
+
 let get_goal_context n =
   let pftree = get_pftreestate () in
   let goal = nth_goal_of_pftreestate n pftree in
@@ -208,7 +211,14 @@ let check_no_pending_proofs () =
 let delete_current_proof () = delete_proof_gen (get_current_proof_name ())
 
 let delete_all_proofs = init_proofs
-   
+
+(*********************************************************************)
+(*   Modifying the end tactic of the current profftree               *)
+(*********************************************************************)
+let set_end_tac tac =
+  let top = get_topstate () in
+  top.top_end_tac <- Some tac
+
 (*********************************************************************)
 (*              Modifying the current prooftree                      *)
 (*********************************************************************)
@@ -216,6 +226,7 @@ let delete_all_proofs = init_proofs
 let start_proof na str sign concl hook =
   let top_goal = mk_goal sign concl in
   let ts = { 
+    top_end_tac = None;
     top_hyps = (sign,empty_named_context);
     top_goal = top_goal;
     top_strength = str;
@@ -224,9 +235,10 @@ let start_proof na str sign concl hook =
   start(na,ts);
   set_current_proof na
 
+
 let solve_nth k tac =
-  let pft = get_pftreestate() in
-  if not (List.mem (-1) (cursor_of_pftreestate pft)) then 
+  let pft = get_pftreestate () in
+  if not (List.mem (-1) (cursor_of_pftreestate pft)) then
     mutate (solve_nth_pftreestate k tac)
   else 
     error "cannot apply a tactic when we are descended behind a tactic-node"
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 8cf1cffe11..9585e7b3c9 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -106,6 +106,9 @@ val set_xml_cook_proof : (pftreestate -> unit) -> unit
 
 val get_pftreestate : unit -> pftreestate
 
+(* [get_end_tac ()] returns the current tactic to apply to all new subgoal *)
+val get_end_tac : unit -> tactic option
+
 (* [get_goal_context n] returns the context of the [n]th subgoal of
    the current focused proof or raises a [UserError] if there is no
    focused proof or if there is no more subgoals *)
@@ -125,6 +128,11 @@ val get_current_proof_name : unit -> identifier
 
 val get_all_proof_names : unit -> identifier list
 
+(*s [set_end_tac tac] applies tactic [tac] to all subgoal generate
+    by [solve_nth] *)
+
+val set_end_tac : tactic -> unit
+
 (*s [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 *)