Merge remote-tracking branch 'github/pr/232' into v8.6

Was PR#232: Fix the parsing of goal selectors.

5 files changed, 46 insertions, 22 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 1d89c17f47..587f4e5cb3 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -26,6 +26,7 @@ problems.
 \def\tacarg{\nterm{tacarg}}
 \def\cpattern{\nterm{cpattern}}
 \def\selector{\textrm{\textsl{selector}}}
+\def\toplevelselector{\textrm{\textsl{toplevel\_selector}}}
 
 The syntax of the tactic language is given Figures~\ref{ltac}
 and~\ref{ltac-aux}. See Chapter~\ref{BNF-syntax} for a description of
@@ -105,7 +106,7 @@ is understood as
 & | & {\tt exactly\_once} {\tacexprpref}\\
 & | & {\tt timeout} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\
 & | & {\tt time} \zeroone{\qstring} {\tacexprpref}\\
-& | & {\selector} {\tt :} {\tacexprpref}\\
+& | & {\tt only} {\selector} {\tt :} {\tacexprpref}\\
 & | & {\tacexprinf} \\
 \\
 {\tacexprinf} & ::= &
@@ -209,11 +210,14 @@ is understood as
 \\
 \selector & ::= &
         [{\ident}]\\
-& $|$ & {\tt all}\\
-& $|$ & {\tt par}\\
 & $|$ & {\integer}\\
 & $|$ & \nelist{{\it (}{\integer} {\it |} {\integer} {\tt -} {\integer}{\it )}}
-          {\tt ,}
+          {\tt ,}\\
+\\
+\toplevelselector & ::= &
+        \selector\\
+& $|$ & {\tt all}\\
+& $|$ & {\tt par}
 \end{tabular}
 \end{centerframe}
 \caption{Syntax of the tactic language (continued)}
@@ -374,7 +378,12 @@ for $=1,...,n$. It fails if the number of focused goals is not exactly $n$.
 We can restrict the application of a tactic to a subset of
 the currently focused goals with:
 \begin{quote}
-{\selector} {\tt :} {\tacexpr}
+  {\toplevelselector} {\tt :} {\tacexpr}
+\end{quote}
+We can also use selectors as a tactical, which allows to use them nested in
+a tactic expression, by using the keyword {\tt only}:
+\begin{quote}
+  {\tt only} {\selector} {\tt :} {\tacexpr}
 \end{quote}
 When selecting several goals, the tactic {\tacexpr} is applied globally to
 all selected goals.
@@ -396,11 +405,12 @@ all selected goals.
     of goals described by the given ranges. You can write a single
     $n$ as a shortcut for $n$-$n$ when specifying multiple ranges.
 
-  \item {\tt all: } {\tacexpr}
+  \item {\tt all:} {\tacexpr}
 
     In this variant, {\tacexpr} is applied to all focused goals.
+    {\tt all:} can only be used at the toplevel of a tactic expression.
 
-  \item {\tt par: } {\tacexpr}
+  \item {\tt par:} {\tacexpr}
 
     In this variant, {\tacexpr} is applied to all focused goals
     in parallel.  The number of workers can be controlled via the
@@ -409,7 +419,7 @@ all selected goals.
     on goals containing no existential variables and {\tacexpr} must
     either solve the goal completely or do nothing (i.e. it cannot make
     some progress).
-    {\tt par: } can only be used at the top level of a tactic expression.
+    {\tt par:} can only be used at the toplevel of a tactic expression.
 
 \end{Variants}
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 65b49893b0..c5fd40bf15 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -46,13 +46,13 @@ goal selector (see Section \ref{ltac:selector}).
 If no selector is specified, the default
 selector (see Section \ref{default-selector}) is used.
 
-\newcommand{\selector}{\nterm{selector}}
+\newcommand{\toplevelselector}{\nterm{toplevel\_selector}}
 \begin{tabular}{lcl}
-{\commandtac} & ::= & {\selector} {\tt :} {\tac} {\tt .}\\
+{\commandtac} & ::= & {\toplevelselector} {\tt :} {\tac} {\tt .}\\
  & $|$ & {\tac} {\tt .}
 \end{tabular}
-\subsection[\tt Set Default Goal Selector ``\selector''.]
-           {\tt Set Default Goal Selector ``\selector''.
+\subsection[\tt Set Default Goal Selector ``\toplevelselector''.]
+           {\tt Set Default Goal Selector ``\toplevelselector''.
             \optindex{Default Goal Selector}
             \label{default-selector}}
 After using this command, the default selector -- used when no selector
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index 9f2c0a93e7..a3ca4ebc4a 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -45,7 +45,6 @@ let new_entry name =
   let e = Gram.entry_create name in
   e
 
-let selector = new_entry "vernac:selector"
 let toplevel_selector = new_entry "vernac:toplevel_selector"
 let tacdef_body = new_entry "tactic:tacdef_body"
 
@@ -79,7 +78,7 @@ let warn_deprecated_appcontext =
 
 GEXTEND Gram
   GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg
-          tactic_mode constr_may_eval constr_eval selector toplevel_selector;
+          tactic_mode constr_may_eval constr_eval toplevel_selector;
 
   tactic_then_last:
     [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" ->
@@ -316,13 +315,16 @@ GEXTEND Gram
         l = OPT [","; l = LIST1 range_selector SEP "," -> l] ->
           Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l ] ]
   ;
+  selector_body:
+  [ [ l = range_selector_or_nth -> l
+    | test_bracket_ident; "["; id = ident; "]" -> SelectId id ] ]
+  ;
   selector:
-    [ [ l = range_selector_or_nth; ":" -> l
-      | IDENT "all" ; ":" -> SelectAll ] ]
+    [ [ IDENT "only"; sel = selector_body; ":" -> sel ] ]
   ;
   toplevel_selector:
-    [ [ s = selector -> s
-      | test_bracket_ident; "["; id = ident; "]"; ":" -> SelectId id ] ]
+    [ [ sel = selector_body; ":" -> sel
+    |   IDENT "all"; ":" -> SelectAll ] ]
   ;
   tactic_mode:
     [ [ g = OPT toplevel_selector; tac = G_vernac.subgoal_command -> tac g ] ]
diff --git a/test-suite/bugs/closed/4877.v b/test-suite/bugs/closed/4877.v
new file mode 100644
index 0000000000..7e3c78dc2e
--- /dev/null
+++ b/test-suite/bugs/closed/4877.v
@@ -0,0 +1,12 @@
+Ltac induction_last :=
+  let v := match goal with
+           | |- forall x y, _ = _ -> _ => 1
+           | |- forall x y, _ -> _ = _ -> _ => 2
+           | |- forall x y, _ -> _ -> _ = _ -> _ => 3
+           end in
+  induction v.
+
+Goal forall n m : nat, True -> n = m -> m = n.
+  induction_last.
+  reflexivity.
+Qed.
\ No newline at end of file
diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v
index 91fb54d9a1..8681405175 100644
--- a/test-suite/success/goal_selector.v
+++ b/test-suite/success/goal_selector.v
@@ -34,7 +34,7 @@ Qed.
 
 Goal True -> True.
 Proof.
-  intros y; 1-2 : repeat idtac.
+  intros y; only 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.
@@ -44,12 +44,12 @@ Qed.
 Goal True /\ (True /\ True).
 Proof.
   dup.
-  - split; 2: (split; exact I).
+  - split; only 2: (split; exact I).
     exact I.
-  - split; 2: split; exact I.
+  - split; only 2: split; exact I.
 Qed.
 
 Goal True -> exists (x : Prop), x.
 Proof.
-  intro H; eexists ?[x]. [x]: exact True. 1: assumption.
+  intro H; eexists ?[x]; only [x]: exact True. 1: assumption.
 Qed.