Make focus command and goal selection for query commands independent …

…of ltac1 Fix #18351
coq · Feb 22, 2024 · 6c416d5 · 6c416d5
1 parent f1e9816
commit 6c416d5
Show file tree

Hide file tree

Showing 6 changed files with 99 additions and 104 deletions.
diff --git a/doc/changelog/08-vernac-commands-and-options/18707-vernac-focus.rst b/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).
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
@@ -836,10 +836,6 @@ STRING: [
 
   (* added productions *)
 
-command_entry: [
-| noedit_mode
-]
-
 DELETE: [
 | tactic_then_locality
 ]
@@ -1738,18 +1734,12 @@ let_clause: [
 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
-| REPLACE OPT toplevel_selector "{"
-(* semantically restricted *)
-| WITH OPT ( [ natural | "[" ident "]" ] ":" ) "{"
-| MOVETO simple_tactic OPT ( [ natural | "[" ident "]" ] ":" ) "{"
-| DELETE simple_tactic
 | DELETENT
 ]
 
@@ -1808,6 +1798,18 @@ vernac_aux: [
 | DELETENT
 ]
 
+subprf: [
+| REPLACE OPT toplevel_selector_temp "{"
+(* semantically restricted *)
+| WITH OPT ( [ natural | "[" ident "]" ] ":" ) "{"
+| MOVEALLBUT simple_tactic
+| OPT toplevel_selector_temp; query_command
+]
+
+subprf: [
+| DELETENT
+]
+
 command: [
 | gallina
 | gallina_ext
@@ -2148,16 +2150,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
 ]
@@ -2263,7 +2255,6 @@ ne_rewstrategy1_list_sep_semicolon: [
 SPLICE: [
 | ne_rewstrategy1_list_sep_semicolon
 | clause
-| noedit_mode
 | match_list
 | match_context_list
 | IDENT
@@ -2515,7 +2506,6 @@ SPLICE: [
 | syntax
 | vernac_control
 | vernac_toplevel
-| command_entry
 | ltac_builtins
 | ltac_constructs
 | ltac2_constructs

diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
@@ -791,14 +791,11 @@ vernac_aux: [
 | command_entry
 ]
 
-noedit_mode: [
-| query_command
-]
-
 subprf: [
 | BULLET
-| "{"
+| OPT toplevel_selector "{"
 | "}"
+| OPT toplevel_selector query_command
 ]
 
 gallina: [
@@ -1282,6 +1279,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 "."
@@ -1543,27 +1561,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
@@ -2235,13 +2232,6 @@ tactic: [
 | ltac_expr5
 ]
 
-tactic_mode: [
-| OPT toplevel_selector G_vernac.query_command
-| OPT toplevel_selector "{"
-| OPT ltac_selector OPT ltac_info tactic ltac_use_default
-| "par" ":" OPT ltac_info tactic ltac_use_default
-]
-
 ltac_selector: [
 | toplevel_selector
 ]
@@ -2255,6 +2245,11 @@ ltac_use_default: [
 | "..."
 ]
 
+tactic_mode: [
+| OPT ltac_selector OPT ltac_info tactic ltac_use_default
+| "par" ":" OPT ltac_info tactic ltac_use_default
+]
+
 ltac_tactic_level: [
 | "(" "at" "level" natural ")"
 ]

diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
@@ -282,11 +282,6 @@ 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) } ] ]
-  ;
   command: TOP
     [ [ IDENT "Proof"; "with"; ta = Pltac.tactic;
         l = OPT [ IDENT "using"; l = G_vernac.section_subset_expr -> { l } ] ->

diff --git a/test-suite/bugs/bug_18351.v b/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.
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
@@ -170,14 +170,13 @@ GRAMMAR EXTEND Gram
   vernac_aux: LAST
     [ [ prfcom = command_entry -> { prfcom } ] ]
   ;
-  noedit_mode:
-    [ [ c = query_command -> { VernacSynPure (c None) } ] ]
-  ;
 
   subprf:
   [ [ s = BULLET -> { VernacBullet (make_bullet s) }
-    | "{" -> { VernacSubproof None }
+    | g = OPT toplevel_selector; "{" -> { VernacSubproof g }
     | "}" -> { VernacEndSubproof }
+    (* query_command needs to be here to factor with VernacSubproof *)
+    | g = OPT toplevel_selector; c = query_command -> { c g }
     ] ]
   ;
 
@@ -970,6 +969,45 @@ GRAMMAR EXTEND Gram
 
 END
 
+{
+
+(* Hack to parse "[ id" without dropping [ *)
+let test_bracket_ident =
+  let open Pcoq.Lookahead in
+  to_entry "test_bracket_ident" begin
+    lk_kw "[" >> lk_ident
+  end
+
+}
+
+GRAMMAR EXTEND Gram
+  GLOBAL: toplevel_selector goal_selector;
+  range_selector:
+    [ [ n = natural ; "-" ; m = natural -> { (n, m) }
+      | n = natural -> { (n, n) } ] ]
+  ;
+  (* We unfold a range selectors list once so that we can make a special case
+   * for a unique SelectNth selector. *)
+  range_selector_or_nth:
+    [ [ n = natural ; "-" ; m = natural;
+        l = OPT [","; l = LIST1 range_selector SEP "," -> { l } ] ->
+        { Goal_select.SelectList ((n, m) :: Option.default [] l) }
+      | n = natural;
+        l = OPT [","; l = LIST1 range_selector SEP "," -> { l } ] ->
+        { let open Goal_select in
+          Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l } ] ]
+  ;
+  goal_selector:
+  [ [ l = range_selector_or_nth -> { l }
+    | test_bracket_ident; "["; id = ident; "]" -> { Goal_select.SelectId id } ] ]
+  ;
+  toplevel_selector:
+    [ [ sel = goal_selector; ":" -> { sel }
+    |   "!"; ":" -> { Goal_select.SelectAlreadyFocused }
+    |   IDENT "all"; ":" -> { Goal_select.SelectAll } ] ]
+  ;
+END
+
 GRAMMAR EXTEND Gram
   GLOBAL: command query_command coercion_class gallina_ext search_query search_queries;
 
@@ -1051,7 +1089,7 @@ GRAMMAR EXTEND Gram
       | IDENT "Remove"; table = IDENT; v = LIST1 table_value ->
           { VernacSynPure (VernacRemoveOption ([table], v)) } ]]
   ;
-  query_command: (* TODO: rapprocher Eval et Check *)
+  query_command:
     [ [ IDENT "Eval"; r = red_expr; "in"; c = lconstr; "." ->
           { fun g -> VernacCheckMayEval (Some r, g, c) }
       | IDENT "Compute"; c = lconstr; "." ->
@@ -1383,42 +1421,3 @@ GRAMMAR EXTEND Gram
       | "as"; IDENT "strict"; IDENT "pattern" -> { Notation_term.AsStrictPattern } ] ]
   ;
 END
-
-{
-
-(* Hack to parse "[ id" without dropping [ *)
-let test_bracket_ident =
-  let open Pcoq.Lookahead in
-  to_entry "test_bracket_ident" begin
-    lk_kw "[" >> lk_ident
-  end
-
-}
-
-GRAMMAR EXTEND Gram
-  GLOBAL: toplevel_selector goal_selector;
-  range_selector:
-    [ [ n = natural ; "-" ; m = natural -> { (n, m) }
-      | n = natural -> { (n, n) } ] ]
-  ;
-  (* We unfold a range selectors list once so that we can make a special case
-   * for a unique SelectNth selector. *)
-  range_selector_or_nth:
-    [ [ n = natural ; "-" ; m = natural;
-        l = OPT [","; l = LIST1 range_selector SEP "," -> { l } ] ->
-        { Goal_select.SelectList ((n, m) :: Option.default [] l) }
-      | n = natural;
-        l = OPT [","; l = LIST1 range_selector SEP "," -> { l } ] ->
-        { let open Goal_select in
-          Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l } ] ]
-  ;
-  goal_selector:
-  [ [ l = range_selector_or_nth -> { l }
-    | test_bracket_ident; "["; id = ident; "]" -> { Goal_select.SelectId id } ] ]
-  ;
-  toplevel_selector:
-    [ [ sel = goal_selector; ":" -> { sel }
-    |   "!"; ":" -> { Goal_select.SelectAlreadyFocused }
-    |   IDENT "all"; ":" -> { Goal_select.SelectAll } ] ]
-  ;
-END