diff --git a/dev/ci/user-overlays/18707-SkySkimmer-vernac-focus.sh b/dev/ci/user-overlays/18707-SkySkimmer-vernac-focus.sh
new file mode 100644
index 000000000000..10536330d03d
--- /dev/null
+++ b/dev/ci/user-overlays/18707-SkySkimmer-vernac-focus.sh
@@ -0,0 +1 @@
+overlay mtac2 https://github.com/SkySkimmer/Mtac2 vernac-focus 18707
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
new file mode 100644
index 000000000000..592690c00cdd
--- /dev/null
+++ 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
index 953b56b0b355..2140445e0286 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/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
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 991b8a9f1f2c..6c5cbceb0653 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/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: [
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 841fa620f21e..ff754682edd3 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -201,7 +201,6 @@ REACHABLE: [
 NOTINRSTS: [
 | command
 | control_command
-| query_command
 | simple_tactic
 | hints_regexp
 | REACHABLE
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index c840ab3547e2..e8895945932c 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/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;
diff --git a/plugins/ltac2/g_ltac2.mlg b/plugins/ltac2/g_ltac2.mlg
index dfeac52a4c64..299656fe2b35 100644
--- a/plugins/ltac2/g_ltac2.mlg
+++ b/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
 
 {
diff --git a/test-suite/bugs/bug_12138.v b/test-suite/bugs/bug_12138.v
deleted file mode 100644
index ac5c89d96cc0..000000000000
--- a/test-suite/bugs/bug_12138.v
+++ /dev/null
@@ -1,2 +0,0 @@
-Fail {
-Fail }
diff --git a/test-suite/bugs/bug_18351.v b/test-suite/bugs/bug_18351.v
new file mode 100644
index 000000000000..6e19705d7b6b
--- /dev/null
+++ 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/test-suite/output-coqtop/bug_12138.out b/test-suite/output-coqtop/bug_12138.out
new file mode 100644
index 000000000000..85fb63991115
--- /dev/null
+++ b/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.
+
+
diff --git a/test-suite/output-coqtop/bug_12138.v b/test-suite/output-coqtop/bug_12138.v
new file mode 100644
index 000000000000..d671d3991716
--- /dev/null
+++ b/test-suite/output-coqtop/bug_12138.v
@@ -0,0 +1,5 @@
+{
+
+Comments. (* coqtop parsing recovery skips to the dot *)
+
+}
diff --git a/test-suite/success/subprf_commands.v b/test-suite/success/subprf_commands.v
new file mode 100644
index 000000000000..269c2c17434b
--- /dev/null
+++ b/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.
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 86d2513ef45d..fee9eae4be22 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -41,6 +41,7 @@ let search_query = Entry.make "search_query"
 let search_queries = Entry.make "search_queries"
 
 let subprf = Entry.make "subprf"
+let subprf_with_selector = Entry.make "subprf_with_selector"
 
 let quoted_attributes = Entry.make "quoted_attributes"
 let attribute_list = Entry.make "attribute_list"
@@ -92,7 +93,7 @@ let test_id_colon =
 }
 
 GRAMMAR EXTEND Gram
-  GLOBAL: vernac_control quoted_attributes attribute_list gallina_ext noedit_mode subprf;
+  GLOBAL: vernac_control quoted_attributes attribute_list gallina_ext noedit_mode subprf subprf_with_selector;
   vernac_control: FIRST
     [ [ IDENT "Time"; c = vernac_control ->
         { add_control_flag ~loc ~flag:ControlTime c }
@@ -164,22 +165,26 @@ GRAMMAR EXTEND Gram
       | g = gallina_ext; "." -> { g }
       | c = command; "." -> { c }
       | c = syntax; "." -> { c }
-      | c = subprf -> { VernacSynPure c }
     ] ]
   ;
   vernac_aux: LAST
     [ [ prfcom = command_entry -> { prfcom } ] ]
   ;
-  noedit_mode:
-    [ [ c = query_command -> { VernacSynPure (c None) } ] ]
+
+  noedit_mode: [ [ c = query_command -> { VernacSynPure (c None) } ] ]
   ;
 
   subprf:
   [ [ s = BULLET -> { VernacBullet (make_bullet s) }
-    | "{" -> { VernacSubproof None }
     | "}" -> { VernacEndSubproof }
     ] ]
   ;
+  subprf_with_selector:
+  [ [ "{" -> { fun g -> VernacSubproof g }
+    (* query_command needs to be here to factor with VernacSubproof *)
+    | c = query_command -> { c }
+    ] ]
+  ;
 
 END
 
@@ -970,6 +975,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 +1095,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 +1427,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
diff --git a/vernac/g_vernac.mli b/vernac/g_vernac.mli
index f1be26af9cd2..f74219b753f4 100644
--- a/vernac/g_vernac.mli
+++ b/vernac/g_vernac.mli
@@ -18,6 +18,7 @@ val search_queries :
     Pcoq.Entry.t
 
 val subprf : Vernacexpr.synpure_vernac_expr Pcoq.Entry.t
+val subprf_with_selector : (Goal_select.t option -> Vernacexpr.synpure_vernac_expr) Pcoq.Entry.t
 
 val quoted_attributes : Attributes.vernac_flags Pcoq.Entry.t