Adds a new goal selector "all:".

all:tac applies tac to all the focused subgoals.

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

2 files changed, 21 insertions, 14 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 6c0ddfc11a..5d053e4c87 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -90,19 +90,25 @@ let current_proof_statement () =
     | (id,([concl],strength,hook)) -> id,strength,concl,hook
     | _ -> Errors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement")
 
-let solve_nth ?with_end_tac gi tac pr =
+let solve ?with_end_tac gi tac pr =
   try 
     let tac = match with_end_tac with
       | None -> tac
       | Some etac -> Proofview.tclTHEN tac etac in
-    Proof.run_tactic (Global.env ()) (Proofview.tclFOCUS gi gi tac) pr
+    let tac = match gi with
+      | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac
+      | Vernacexpr.SelectAll -> tac
+    in
+    Proof.run_tactic (Global.env ()) tac pr
   with
     | Proof_global.NoCurrentProof  -> Errors.error "No focused proof"
-    | Proofview.IndexOutOfRange ->
-	let msg = str "No such goal: " ++ int gi ++ str "." in
-	Errors.errorlabstrm "" msg
+    | Proofview.IndexOutOfRange -> 
+        match gi with
+	| Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in
+	                            Errors.errorlabstrm "" msg
+        | _ -> assert false
 
-let by tac = Proof_global.with_current_proof (fun _ -> solve_nth 1 tac)
+let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) tac)
 
 let instantiate_nth_evar_com n com = 
   Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.instantiate_evar n com p)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 73f12db987..f7c7b36537 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -120,7 +120,7 @@ val get_all_proof_names : unit -> Id.t list
 
 (** {6 ... } *)
 (** [set_end_tac tac] applies tactic [tac] to all subgoal generate
-    by [solve_nth] *)
+    by [solve] *)
 
 val set_end_tac : Tacexpr.raw_tactic_expr -> unit
 
@@ -131,17 +131,18 @@ val set_used_variables : Id.t list -> unit
 val get_used_variables : unit -> Context.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 *)
+(** [solve (SelectNth 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. [solve SelectAll
+    tac] applies [tac] to all subgoals. *)
 
-val solve_nth : ?with_end_tac:unit Proofview.tactic -> int -> unit Proofview.tactic ->
+val solve : ?with_end_tac:unit Proofview.tactic -> Vernacexpr.goal_selector -> unit Proofview.tactic ->
       Proof.proof -> Proof.proof*bool
 
 (** [by tac] applies tactic [tac] to the 1st subgoal of the current
-   focused proof or raises a UserError if there is no focused proof or
-   if there is no more subgoals.
-   Returns [false] if an unsafe tactic has been used. *)
+    focused proof or raises a UserError if there is no focused proof or
+    if there is no more subgoals.
+    Returns [false] if an unsafe tactic has been used. *)
 
 val by : unit Proofview.tactic -> bool