Merge PR #18707: Make focus command and goal selection for query comm…

…ands independent of ltac1

Reviewed-by: ppedrot
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

dev/ci/user-overlays/18707-SkySkimmer-vernac-focus.sh

@@ -0,0 +1 @@
+overlay mtac2 https://github.com/SkySkimmer/Mtac2 vernac-focus 18707

doc/changelog/08-vernac-commands-and-options/18707-vernac-focus.rst

@@ -0,0 +1,6 @@
+- **Changed:**
+  focus commands such as `1:{` and goal selection for query commands such as `1: Check`
+  do not need `Classic` (Ltac1) proof mode to function. In particular they function in Ltac2 mode
+  (`#18707 <https://github.com/coq/coq/pull/18707>`_,
+  fixes `#18351 <https://github.com/coq/coq/issues/18351>`_,
+  by Gaëtan Gilbert).

doc/tools/docgram/common.edit_mlg

@@ -109,7 +109,6 @@ RENAME: [
 | Constr.global global
 | Constr.lconstr lconstr
 | Constr.cpattern cpattern
-| G_vernac.query_command query_command
 | G_vernac.section_subset_expr section_var_expr
 | Prim.ident ident
 | Prim.reference reference
@@ -1736,24 +1735,35 @@ let_clause: [
 | WITH name  ":=" ltac_expr5
 ]
 
+subprf_with_selector: [
+| DELETE query_command
+]
+
+SPLICE: [
+| subprf_with_selector
+]
+
 tactic_mode: [
 (* todo: make sure to document this production! *)
 (* deleting to allow splicing query_command into command *)
-| DELETE OPT toplevel_selector query_command
 | DELETE OPT ltac_selector OPT ltac_info tactic ltac_use_default
 | DELETE "par" ":" OPT ltac_info tactic ltac_use_default
 (* Ignore attributes (none apply) and "...". *)
 | ltac_info tactic
 | MOVETO command ltac_info tactic
-| DELETE command
+| MOVETO simple_tactic subprf
 | REPLACE OPT toplevel_selector "{"
 (* semantically restricted *)
 | WITH OPT ( [ natural | "[" ident "]" ] ":" ) "{"
 | MOVETO simple_tactic OPT ( [ natural | "[" ident "]" ] ":" ) "{"
-| DELETE simple_tactic
+| DELETE command
 | DELETENT
 ]
 
+SPLICE: [
+| subprf
+]
+
 ltac2_scope: [
 | REPLACE syn_node      (* Ltac2 plugin *)
 | WITH name TAG Ltac2
@@ -1805,7 +1815,6 @@ vernac_aux: [
 | DELETE gallina_ext "."
 | DELETE syntax "."
 | DELETE command_entry
-| DELETE subprf
 | DELETENT
 ]
 
@@ -2149,16 +2158,6 @@ simple_binding: [
 | DELETE "(" natural ":=" lconstr ")"
 ]
 
-
-subprf: [
-| MOVEALLBUT simple_tactic
-| "{" (* should be removed.  See https://github.com/coq/coq/issues/12004 *)
-]
-
-subprf: [
-| DELETENT
-]
-
 ltac2_expr: [
 | DELETE _ltac2_expr
 ]
@@ -2532,7 +2531,6 @@ REACHABLE: [
 NOTINRSTS: [
 | command
 | control_command
-| query_command
 | simple_tactic
 | hints_regexp (* manually inserted *)
 | REACHABLE

doc/tools/docgram/fullGrammar

@@ -792,7 +792,6 @@ vernac_aux: [
 | gallina_ext "."
 | command "."
 | syntax "."
-| subprf
 | command_entry
 ]
 
@@ -802,10 +801,14 @@ noedit_mode: [
 
 subprf: [
 | BULLET
-| "{"
 | "}"
 ]
 
+subprf_with_selector: [
+| "{"
+| query_command
+]
+
 gallina: [
 | thm_token ident_decl binders ":" lconstr LIST0 [ "with" ident_decl binders ":" lconstr ]
 | assumption_token inline assum_list
@@ -1287,6 +1290,27 @@ simple_reserv: [
 | LIST1 identref ":" lconstr
 ]
 
+range_selector: [
+| natural "-" natural
+| natural
+]
+
+range_selector_or_nth: [
+| natural "-" natural OPT [ "," LIST1 range_selector SEP "," ]
+| natural OPT [ "," LIST1 range_selector SEP "," ]
+]
+
+goal_selector: [
+| range_selector_or_nth
+| test_bracket_ident "[" ident "]"
+]
+
+toplevel_selector: [
+| goal_selector ":"
+| "!" ":"
+| "all" ":"
+]
+
 query_command: [
 | "Eval" red_expr "in" lconstr "."
 | "Compute" lconstr "."
@@ -1548,27 +1572,6 @@ binder_interp: [
 | "as" "strict" "pattern"
 ]
 
-range_selector: [
-| natural "-" natural
-| natural
-]
-
-range_selector_or_nth: [
-| natural "-" natural OPT [ "," LIST1 range_selector SEP "," ]
-| natural OPT [ "," LIST1 range_selector SEP "," ]
-]
-
-goal_selector: [
-| range_selector_or_nth
-| test_bracket_ident "[" ident "]"
-]
-
-toplevel_selector: [
-| goal_selector ":"
-| "!" ":"
-| "all" ":"
-]
-
 simple_tactic: [
 | "btauto"
 | "congruence" OPT natural
@@ -2241,8 +2244,8 @@ tactic: [
 ]
 
 tactic_mode: [
-| OPT toplevel_selector G_vernac.query_command
-| OPT toplevel_selector "{"
+| subprf
+| OPT toplevel_selector subprf_with_selector
 | OPT ltac_selector OPT ltac_info tactic ltac_use_default
 | "par" ":" OPT ltac_info tactic ltac_use_default
 ]
@@ -3348,7 +3351,8 @@ ltac2_use_default: [
 tac2mode: [
 | OPT ltac2_selector ltac2_expr6 ltac2_use_default      (* ltac2 plugin *)
 | "par" ":" ltac2_expr6 ltac2_use_default      (* ltac2 plugin *)
-| G_vernac.query_command      (* ltac2 plugin *)
+| subprf      (* ltac2 plugin *)
+| OPT toplevel_selector subprf_with_selector      (* ltac2 plugin *)
 ]
 
 ltac1_expr_in_env: [

doc/tools/docgram/orderedGrammar

@@ -201,7 +201,6 @@ REACHABLE: [
 NOTINRSTS: [
 | command
 | control_command
-| query_command
 | simple_tactic
 | hints_regexp
 | REACHABLE

plugins/ltac/g_ltac.mlg

@@ -61,13 +61,15 @@ let for_extraargs = ()
 
 let goal_selector = G_vernac.goal_selector
 let toplevel_selector = G_vernac.toplevel_selector
+let subprf = G_vernac.subprf
+let subprf_with_selector = G_vernac.subprf_with_selector
 
 }
 
 GRAMMAR EXTEND Gram
   GLOBAL: tactic tacdef_body ltac_expr tactic_value command hint
           tactic_mode constr_may_eval constr_eval
-          term;
+          term subprf subprf_with_selector;
 
   tactic_then_last:
     [ [ "|"; lta = LIST0 (OPT ltac_expr) SEP "|" ->
@@ -282,10 +284,10 @@ GRAMMAR EXTEND Gram
   tactic:
     [ [ tac = ltac_expr -> { tac } ] ]
   ;
-
   tactic_mode:
-    [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> { Vernacexpr.VernacSynPure (tac g) }
-      | g = OPT toplevel_selector; "{" -> { Vernacexpr.VernacSynPure (Vernacexpr.VernacSubproof g) } ] ]
+    [ [ p = subprf -> { Vernacexpr.VernacSynPure p }
+      | g = OPT toplevel_selector; p = subprf_with_selector -> { Vernacexpr.VernacSynPure (p g) }
+      ] ]
   ;
   command: TOP
     [ [ IDENT "Proof"; "with"; ta = Pltac.tactic;

plugins/ltac2/g_ltac2.mlg

@@ -1030,6 +1030,9 @@ let pr_ltac2_selector s = Pp.(Goal_select.pr_goal_selector s ++ str ":")
 let pr_ltac2_use_default b =
   if b then (* Bug: a space is inserted before "..." *) str ".." else mt ()
 
+let subprf = G_vernac.subprf
+let subprf_with_selector = G_vernac.subprf_with_selector
+
 }
 
 VERNAC ARGUMENT EXTEND ltac2_selector PRINTED BY { pr_ltac2_selector }
@@ -1055,7 +1058,9 @@ END
 GRAMMAR EXTEND Gram
   GLOBAL: tac2mode;
   tac2mode: TOP
-    [ [ tac = G_vernac.query_command -> { Vernacexpr.VernacSynPure (tac None) } ] ];
+    [ [ p = subprf -> { Vernacexpr.VernacSynPure p }
+      | g = OPT toplevel_selector; p = subprf_with_selector -> { Vernacexpr.VernacSynPure (p g) }
+      ] ];
 END
 
 {

test-suite/bugs/bug_18351.v

@@ -0,0 +1,10 @@
+Require Import Ltac2.Ltac2.
+
+Set Default Goal Selector "!".
+
+Goal True /\ True.
+  split.
+  Fail exact I. (* not focused *)
+  1:{ exact I. }
+  exact I.
+Qed.

test-suite/output-coqtop/bug_12138.out

@@ -0,0 +1,12 @@
+
+Coq < Coq < Coq < Toplevel input, characters 0-1:
+> {
+> ^
+Error: Syntax error: illegal begin of toplevel:vernac_toplevel.
+
+Coq < Coq < Coq < Toplevel input, characters 58-59:
+> }
+> ^
+Error: Syntax error: illegal begin of toplevel:vernac_toplevel.
+
+

test-suite/output-coqtop/bug_12138.v

@@ -0,0 +1,5 @@
+{
+
+Comments. (* coqtop parsing recovery skips to the dot *)
+
+}

test-suite/success/subprf_commands.v

@@ -0,0 +1,17 @@
+Check True.
+Goal True /\ True.
+  Check True.
+  1:Check True.
+  1: idtac.
+  1:{ admit. }
+Abort.
+
+Require Import Ltac2.Ltac2.
+
+Check True.
+Goal True /\ True.
+  Check True.
+  1:Check True.
+  1: ().
+  1:{ admit. }
+Abort.