Fully removing binder_tactic.

Villetaneuse · Dec 6, 2023 · 2bd0e5b · 2bd0e5b
1 parent 3c1cf6c
commit 2bd0e5b
Show file tree

Hide file tree

Showing 7 changed files with 3 additions and 17 deletions.
diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md
@@ -44,15 +44,15 @@ for documentation purposes:
     ```
     ltac_expr:
       [ "5" RIGHTA
-        [ te = binder_tactic -> { te } ]
+        [ ... ]
       [ "4"   ...
     ```
 
     becomes
 
     ```
     tactic_expr5: [
-    | binder_tactic
+    | ...
     | tactic_expr4
     ]
     ```

diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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