Make focus command and goal selection for query commands independent …

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

Hide file tree

Showing 4 changed files with 60 additions and 48 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/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,15 @@ GRAMMAR EXTEND Gram
   vernac_aux: LAST
     [ [ prfcom = command_entry -> { prfcom } ] ]
   ;
-  noedit_mode:
-    [ [ c = query_command -> { VernacSynPure (c None) } ] ]
+  noedit_mode: [ [ "BOOM"; "." -> { assert false } ] ]
   ;
 
   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 +971,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 +1091,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 +1423,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