9 files changed, 42 insertions, 9 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 379dd59d39..c15ef0dd44 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -34,6 +34,12 @@ type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use
 
 type debug = Debug | Info | Off (* for trivial / auto / eauto ... *)
 
+type goal_selector =
+  | SelectNth of int
+  | SelectList of (int * int) list
+  | SelectId of Id.t
+  | SelectAll
+
 type 'a core_induction_arg =
   | ElimOnConstr of 'a
   | ElimOnIdent of Id.t located
@@ -269,6 +275,7 @@ and 'a gen_tactic_expr =
       ('p,'a gen_tactic_expr) match_rule list
   | TacFun of 'a gen_tactic_fun_ast
   | TacArg of 'a gen_tactic_arg located
+  | TacSelect of goal_selector * 'a gen_tactic_expr
   (* For ML extensions *)
   | TacML of Loc.t * ml_tactic_entry * 'a gen_tactic_arg list
   (* For syntax extensions *)
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 029ee8a480..8bae8fcb63 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -27,7 +27,7 @@ type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
    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 =
+type goal_selector = Tacexpr.goal_selector =
   | SelectNth of int
   | SelectList of (int * int) list
   | SelectId of Id.t
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index 3b9c58ceb1..5f52b67119 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -119,7 +119,8 @@ GEXTEND Gram
 (*To do: put Abstract in Refiner*)
       | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None)
       | IDENT "abstract"; tc = NEXT; "using";  s = ident ->
-          TacAbstract (tc,Some s) ]
+          TacAbstract (tc,Some s)
+      | sel = selector; ta = tactic_expr -> TacSelect (sel, ta) ]
 (*End of To do*)
     | "2" RIGHTA
       [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> TacOr (ta0,ta1)
@@ -305,15 +306,15 @@ GEXTEND Gram
   range_selector_or_nth:
     [ [ n = natural ; "-" ; m = natural;
         l = OPT [","; l = LIST1 range_selector SEP "," -> l] ->
-          Vernacexpr.SelectList ((n, m) :: Option.default [] l)
+          SelectList ((n, m) :: Option.default [] l)
       | n = natural;
         l = OPT [","; l = LIST1 range_selector SEP "," -> l] ->
-          Option.cata (fun l -> Vernacexpr.SelectList ((n, n) :: l)) (Vernacexpr.SelectNth n) l ] ]
+          Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l ] ]
   ;
   selector:
     [ [ l = range_selector_or_nth; ":" -> l
-      | test_bracket_ident; "["; id = ident; "]"; ":" -> Vernacexpr.SelectId id
-      | IDENT "all" ; ":" -> Vernacexpr.SelectAll ] ]
+      | "?" ; test_bracket_ident; "["; id = ident; "]"; ":" -> SelectId id
+      | IDENT "all" ; ":" -> SelectAll ] ]
   ;
   tactic_mode:
     [ [ g = OPT selector; tac = G_vernac.subgoal_command -> tac g ] ]
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index 7cda7d1377..a72fb0d061 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -624,6 +624,8 @@ and intern_tactic_seq onlytac ist = function
   | TacSolve l -> ist.ltacvars, TacSolve (List.map (intern_pure_tactic ist) l)
   | TacComplete tac -> ist.ltacvars, TacComplete (intern_pure_tactic ist tac)
   | TacArg (loc,a) -> ist.ltacvars, intern_tactic_as_arg loc onlytac ist a
+  | TacSelect (sel, tac) ->
+      ist.ltacvars, TacSelect (sel, intern_pure_tactic ist tac)
 
   (* For extensions *)
   | TacAlias (loc,s,l) ->
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index ab61c8abba..56812b5546 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1252,6 +1252,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
            strbrk "There is an \"Info\" command to replace it." ++fnl () ++
 	   strbrk "Some specific verbose tactics may also exist, such as info_eauto.");
       eval_tactic ist tac
+  | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
   (* For extensions *)
   | TacAlias (loc,s,l) ->
       let (ids, body) = Tacenv.interp_alias s in
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 7f904a561d..3d51623eaa 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -476,6 +476,13 @@ module New = struct
   let tclPROGRESS t =
     Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t)
 
+  (* Select a subset of the goals *)
+  let tclSELECT = function
+    | Tacexpr.SelectNth i -> Proofview.tclFOCUS i i
+    | Tacexpr.SelectList l -> Proofview.tclFOCUSLIST l
+    | Tacexpr.SelectId id -> Proofview.tclFOCUSID id
+    | Tacexpr.SelectAll -> fun tac -> tac
+
   (* Check that holes in arguments have been resolved *)
 
   let check_evars env sigma extsigma origsigma =
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 0f926468b9..cfdc2cffd4 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -221,6 +221,7 @@ module New : sig
   val tclCOMPLETE : 'a tactic -> 'a tactic
   val tclSOLVE : unit tactic list -> unit tactic
   val tclPROGRESS : unit tactic -> unit tactic
+  val tclSELECT : goal_selector -> 'a tactic -> 'a tactic
   val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic
   val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic
 
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 90a60daa66..fd71f3c423 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -106,7 +106,7 @@ Goal exists x, S 0 = S x.
 eexists ?[x].
 destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *)
 change (0 = S ?x).
-[x]: exact 0. (* Incidentally test applying a tactic to a goal on the shelve *)
+?[x]: exact 0. (* Incidentally test applying a tactic to a goal on the shelve *)
 Abort.
 
 Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n.
diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v
index 9ba748e2a5..dd7ad10131 100644
--- a/test-suite/success/goal_selector.v
+++ b/test-suite/success/goal_selector.v
@@ -34,8 +34,22 @@ Qed.
 
 Goal True -> True.
 Proof.
-  intros y.
+  intros y; 1-2 : repeat idtac.
+  1-1:match goal with y : _ |- _ => let x := y in idtac x end.
   Fail 1-1:let x := y in idtac x.
   1:let x := y in idtac x.
   exact I.
-Qed.
-\ No newline at end of file
+Qed.
+
+Goal True /\ (True /\ True).
+Proof.
+  dup.
+  - split; 2: (split; exact I).
+    exact I.
+  - split; 2: split; exact I.
+Qed.
+
+Goal True -> exists (x : Prop), x.
+Proof.
+  intro H; eexists ?[x]; ?[x]: exact True; assumption.
+Qed.