diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md
index e5ca33380fe2..05a5a4f33f5f 100644
--- a/doc/tools/docgram/README.md
+++ b/doc/tools/docgram/README.md
@@ -44,7 +44,7 @@ for documentation purposes:
     ```
     ltac_expr:
       [ "5" RIGHTA
-        [ te = binder_tactic -> { te } ]
+        [ ... ]
       [ "4"   ...
     ```
 
@@ -52,7 +52,7 @@ for documentation purposes:
 
     ```
     tactic_expr5: [
-    | binder_tactic
+    | ...
     | tactic_expr4
     ]
     ```
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 7394cde15159..de027b385a55 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -2100,9 +2100,6 @@ failkw: [
 | "gfail"
 ]
 
-binder_tactic: [
-]
-
 tactic_arg: [
 | tactic_value
 | Constr.constr
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 4a17f25096aa..b4a879d7e163 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -2226,9 +2226,6 @@ ltac_expr0: [
 | tactic_atom
 ]
 
-binder_tactic: [
-]
-
 tactic_atom: [
 | integer
 | qualid
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 17f730dfe21b..118ac6d928b8 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -70,7 +70,7 @@ let for_extraargs = ()
 }
 
 GRAMMAR EXTEND Gram
-  GLOBAL: tactic tacdef_body ltac_expr binder_tactic tactic_value command hint
+  GLOBAL: tactic tacdef_body ltac_expr tactic_value command hint
           tactic_mode constr_may_eval constr_eval toplevel_selector
           term;
 
@@ -164,11 +164,6 @@ GRAMMAR EXTEND Gram
   failkw:
   [ [ IDENT "fail" -> { TacLocal } | IDENT "gfail" -> { TacGlobal } ] ]
   ;
-  (* binder_tactic: level 1 of ltac_expr *)
-  binder_tactic:
-    [ RIGHTA
-      [ ] ]
-  ;
   (* Tactic arguments to the right of an application *)
   tactic_arg:
     [ [ a = tactic_value -> { a }
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index f37212e2a234..bfdd9814137a 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -40,7 +40,6 @@ let clause_dft_concl =
 (* Main entries for ltac *)
 let tactic_value = Entry.make "tactic_value"
 let ltac_expr = Entry.make "ltac_expr"
-let binder_tactic = Entry.make "binder_tactic"
 
 let tactic = Entry.make "tactic"
 
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index dc7639356f9d..a3b0a313a0bf 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -34,6 +34,5 @@ val in_clause : Names.lident Locus.clause_expr Entry.t
 val clause_dft_concl : Names.lident Locus.clause_expr Entry.t
 val tactic_value : raw_tactic_arg Entry.t
 val ltac_expr : raw_tactic_expr Entry.t
-val binder_tactic : raw_tactic_expr Entry.t
 val tactic : raw_tactic_expr Entry.t
 val tactic_eoi : raw_tactic_expr Entry.t
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index ee3f6da69bbd..4ba0ef0b9a8e 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -620,7 +620,6 @@ let () =
   let open Pcoq.Entry in
   let entries = [
     Any Pltac.ltac_expr;
-    Any Pltac.binder_tactic;
     Any Pltac.simple_tactic;
     Any Pltac.tactic_value;
   ] in