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

7 files changed, 61 insertions, 22 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 2e23d22732..2f76df0e5b 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -25,6 +25,15 @@ type lreference = reference
 
 type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
 
+(* spiwack: I'm choosing, for now, to have [goal_selector] be a
+   different type than [goal_reference] mostly because if it makes sense
+   to print a goal that is out of focus (or already solved) it doesn't
+   make sense to apply a tactic to it. Hence it the types may look very
+   similar, they do not seem to mean the same thing. *)
+type goal_selector =
+  | SelectNth of int
+  | SelectAll
+
 type goal_identifier = string
 type scope_name = string
 
@@ -325,7 +334,7 @@ type vernac_expr =
 
   (* Solving *)
 
-  | VernacSolve of int * raw_tactic_expr * bool
+  | VernacSolve of goal_selector * raw_tactic_expr * bool
   | VernacSolveExistential of int * constr_expr
 
   (* Auxiliary file and library management *)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 1288e2e79c..502b6b8ea3 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -109,8 +109,14 @@ GEXTEND Gram
   noedit_mode:
     [ [ c = subgoal_command -> c None] ]
   ;
+
+  selector:
+    [ [ n=natural; ":" -> SelectNth n
+      | IDENT "all" ; ":" -> SelectAll ] ]
+  ;
+
   tactic_mode:
-  [ [ gln = OPT[n=natural; ":" -> n];
+  [ [ gln = OPT selector;
       tac = subgoal_command -> tac gln ] ]
   ;
 
@@ -127,11 +133,22 @@ GEXTEND Gram
 
 
   subgoal_command: 
-    [ [ c = check_command; "." -> fun g -> c g
+    [ [ c = check_command; "." ->
+                  begin function
+                    | Some (SelectNth g) -> c (Some g)
+                    | None -> c None
+                    | _ ->
+                        (* arnaud: the error is raised bizarely:
+                           "all:Check 0." doesn't do anything, then
+                           inputing anything that ends with a period
+                           (including " .") raises the error. *)
+                        error "Typing and evaluation commands, cannot be used with the \"all:\" selector."
+                  end
       | tac = Tactic.tactic;
         use_dft_tac = [ "." -> false | "..." -> true ] ->
-          (fun g ->
-            let g = Option.default 1 g in
+        (fun g ->
+            (* arnaud: attention �à choisir le bon d�éfaut. *)
+            let g = Option.default (SelectNth 1) g in
             VernacSolve(g,tac,use_dft_tac)) ] ]
   ;
   located_vernac:
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index a3a2b25e44..27d801059a 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -132,7 +132,7 @@ GEXTEND Gram
   GLOBAL: proof_mode ;
 
   proof_mode: LAST
-    [ [ c=G_vernac.subgoal_command -> c (Some 1) ] ]
+    [ [ c=G_vernac.subgoal_command -> c (Some (Vernacexpr.SelectNth 1)) ] ]
   ;
 END  
 
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 6cfa6d47f1..1ffa8275a4 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -773,7 +773,13 @@ let rec pr_vernac = function
 	     prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
   (* Solving *)
   | VernacSolve (i,tac,deftac) ->
-      (if Int.equal i 1 then mt() else int i ++ str ": ") ++
+      let pr_goal_selector = function
+        | SelectNth i -> int i ++ str":"
+        | SelectAll -> str"all" ++ str":"
+      in
+      (* arnaud: attention à imprimer correctement en fonction
+         de la (future) option pour le sélecteur par défaut *)
+      (if i = SelectNth 1 then mt() else pr_goal_selector i) ++
       pr_raw_tactic tac
       ++ (if deftac then str ".." else mt ())
   | VernacSolveExistential (i,c) ->
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
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 62243781ae..f3298c29b9 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -777,7 +777,7 @@ let vernac_solve n tcom b =
     error "Unknown command of the non proof-editing mode.";
   let status = Proof_global.with_current_proof (fun etac p ->
     let with_end_tac = if b then Some etac else None in
-    let (p,status) = solve_nth n (Tacinterp.hide_interp tcom None) ?with_end_tac p in
+    let (p,status) = solve n (Tacinterp.hide_interp tcom None) ?with_end_tac p in
     (* in case a strict subtree was completed,
        go back to the top of the prooftree *)
     let p = Proof.maximal_unfocus command_focus p in