Add syntax [id]: to apply tactic to goal named id.

7 files changed, 25 insertions, 1 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index b784bc433..009ec543c 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -30,6 +30,7 @@ type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
    similar, they do not seem to mean the same thing. *)
 type goal_selector =
   | SelectNth of int
+  | SelectId of Id.t
   | SelectAll
   | SelectAllParallel
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 9fb7c8926..955179ba0 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -127,6 +127,7 @@ GEXTEND Gram
 
   selector:
     [ [ n=natural; ":" -> SelectNth n
+      | "["; id = ident; "]"; ":" -> SelectId id
       | IDENT "all" ; ":" -> SelectAll
       | IDENT "par" ; ":" -> SelectAllParallel ] ]
   ;
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 930166524..b7ac274b7 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -769,6 +769,7 @@ let rec pr_vernac = function
   | VernacSolve (i,tac,deftac) ->
       let pr_goal_selector = function
         | SelectNth i -> int i ++ str":"
+        | SelectId id -> pr_id id ++ str":"
         | SelectAll -> str"all" ++ str":"
         | SelectAllParallel -> str"par"
       in
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 49195aecc..1b0b2f401 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -94,6 +94,7 @@ let solve ?with_end_tac gi tac pr =
       | Some etac -> Proofview.tclTHEN tac etac in
     let tac = match gi with
       | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac
+      | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac
       | Vernacexpr.SelectAll -> tac
       | Vernacexpr.SelectAllParallel ->
           Errors.anomaly(str"SelectAllParallel not handled by Stm")
@@ -101,7 +102,7 @@ let solve ?with_end_tac gi tac pr =
     Proof.run_tactic (Global.env ()) tac pr
   with
     | Proof_global.NoCurrentProof  -> Errors.error "No focused proof"
-    | Proofview.IndexOutOfRange -> 
+    | Proofview.IndexOutOfRange ->
         match gi with
 	| Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in
 	                            Errors.errorlabstrm "" msg
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 82e176f97..1994922a9 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -528,6 +528,7 @@ let get_default_goal_selector () = !default_goal_selector
 let print_goal_selector = function
   | Vernacexpr.SelectAll -> "all"
   | Vernacexpr.SelectNth i -> string_of_int i
+  | Vernacexpr.SelectId id -> Id.to_string id
   | Vernacexpr.SelectAllParallel -> "par"
 
 let parse_goal_selector = function
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index a5cb2edb8..bc6ce4fc6 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -330,6 +330,23 @@ let tclFOCUS_gen nosuchgoal i j t =
 let tclFOCUS i j t = tclFOCUS_gen (tclZERO (NoSuchGoals (j+1-i))) i j t
 let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t
 
+let tclFOCUSID id t =
+  let (>>=) = Proof.bind in
+  let (>>) = Proof.seq in
+  Proof.get >>= fun initial ->
+  let rec aux n = function
+    | [] -> tclZERO (NoSuchGoals 1)
+    | g::l ->
+        if Names.Id.equal (Goal.goal_ident initial.solution g) id then
+          let (focused,context) = focus n n initial in
+          Proof.set focused >>
+            t >>= fun result ->
+          Proof.modify (fun next -> unfocus context next) >>
+            Proof.ret result
+        else
+          aux (n+1) l in
+  aux 1 initial.comb
+
 
 (* Dispatch tacticals are used to apply a different tactic to each goal under
    consideration. They come in two flavours:
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index b1ff30ee9..3b2dd7ccd 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -197,6 +197,8 @@ val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic
 exception NoSuchGoals of int
 val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
 
+val tclFOCUSID : Names.Id.t -> 'a tactic -> 'a tactic
+
 (* Focuses a tactic at a range of subgoals, found by their indices.
    The other goals are restored to the focus when the tactic is done.