Merge PR coq#18386: Fix binder_tactic after coq#18220 (see coq#18368)

Reviewed-by: proux01 Co-authored-by: proux01 <[email protected]>
Villetaneuse · Dec 8, 2023 · e366e49 · e366e49
2 parents db970b7 + 2bd0e5b
commit e366e49
Show file tree

Hide file tree

Showing 12 changed files with 28 additions and 48 deletions.
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
@@ -78,9 +78,7 @@ The constructs in :token:`ltac_expr` are :term:`left associative`.
    | @ltac_expr1 %|| @ltac_expr2
    | @l2_tactic
    | @ltac_expr1
-   ltac_expr1 ::= fun {+ @name } => @ltac_expr
-   | let {? rec } @let_clause {* with @let_clause } in @ltac_expr
-   | @tactic_value
+   ltac_expr1 ::= @tactic_value
    | @qualid {+ @tactic_arg }
    | @l1_tactic
    | @ltac_expr0
@@ -116,12 +114,12 @@ The constructs in :token:`ltac_expr` are :term:`left associative`.
    varying levels in :token:`ltac_expr`.  For simplicity of presentation, the |Ltac| constructs
    are documented as tactics.  Tactics are grouped as follows:
 
-   - :production:`binder_tactic`\s are: :tacn:`fun` and :tacn:`let`
    - :production:`l3_tactic`\s include |Ltac| tactics: :tacn:`try`,
      :tacn:`do`, :tacn:`repeat`, :tacn:`timeout`, :tacn:`time`, :tacn:`progress`, :tacn:`once`,
      :tacn:`exactly_once`, :tacn:`only` and :tacn:`abstract`
    - :production:`l2_tactic`\s are: :tacn:`tryif`
-   - :production:`l1_tactic`\s are the :token:`simple_tactic`\s, :tacn:`first`, :tacn:`solve`,
+   - :production:`l1_tactic`\s are: :tacn:`fun` and :tacn:`let`,
+     the :token:`simple_tactic`\s, :tacn:`first`, :tacn:`solve`,
      :tacn:`idtac`, :tacn:`fail` and
      :tacn:`gfail` as well as :tacn:`match`, :tacn:`match goal` and their :n:`lazymatch` and
      :n:`multimatch` variants.
@@ -293,7 +291,7 @@ Local definitions: let
    Use :tacn:`let` `rec` to create recursive or mutually recursive bindings, which
    causes the definitions to be evaluated lazily.
 
-   :tacn:`let` is a :token:`binder_tactic`.
+   :tacn:`let` is a :token:`l1_tactic`.
 
 Function construction and application
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -306,7 +304,7 @@ local definitions) with:
    Indeed, local definitions of functions are syntactic sugar for binding
    a :n:`fun` tactic to an identifier.
 
-   :tacn:`fun` is a :token:`binder_tactic`.
+   :tacn:`fun` is a :token:`l1_tactic`.
 
 Functions can return values of any type.
 

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -730,10 +730,9 @@ Displaying information about notations
 
      Entry ltac_expr is
      [ "5" RIGHTA
-       [ binder_tactic ]
+       [ ]
      | "4" LEFTA
-       [ SELF; ";"; binder_tactic
-       | SELF; ";"; SELF
+       [ SELF; ";"; SELF
        | SELF; ";"; tactic_then_locality; for_each_goal; "]" ]
      | "3" RIGHTA
        [ IDENT "try"; SELF

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/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
@@ -881,6 +881,8 @@ ltac_expr2: [
 l1_tactic: [ ]
 
 ltac_expr1: [
+| REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr5
+| WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr5
 | EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end"
 | MOVETO simple_tactic match_key OPT "reverse" "goal" "with" match_context_list "end"
 | MOVETO simple_tactic match_key ltac_expr5 "with" match_list "end"
@@ -891,7 +893,6 @@ ltac_expr1: [
 | l1_tactic
 | DELETE simple_tactic
 | MOVEALLBUT ltac_builtins
-| binder_tactic
 | l1_tactic
 | tactic_value
 | reference LIST1 tactic_arg
@@ -1438,11 +1439,6 @@ explicit_subentry: [
 | DELETE "constr"    (* covered by another prod *)
 ]
 
-binder_tactic: [
-| REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr5
-| WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr5
-]
-
 field_body: [
 | REPLACE binders of_type_inst lconstr
 | WITH binders of_type_inst
@@ -1904,7 +1900,6 @@ ltac2_constructs: [
 ]
 
 simple_tactic: [
-| binder_tactic
 | ltac_builtins
 | ltac_constructs
 | ltac2_constructs
@@ -2512,7 +2507,6 @@ SPLICE: [
 | vernac_control
 | vernac_toplevel
 | command_entry
-| binder_tactic
 | ltac_builtins
 | ltac_constructs
 | ltac2_constructs

diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
@@ -2074,7 +2074,8 @@ ltac_expr2: [
 ]
 
 ltac_expr1: [
-| binder_tactic
+| "fun" LIST1 input_fun "=>" ltac_expr5
+| "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr5
 | match_key "goal" "with" match_context_list "end"
 | match_key "reverse" "goal" "with" match_context_list "end"
 | match_key ltac_expr5 "with" match_list "end"
@@ -2099,11 +2100,6 @@ failkw: [
 | "gfail"
 ]
 
-binder_tactic: [
-| "fun" LIST1 input_fun "=>" ltac_expr5
-| "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr5
-]
-
 tactic_arg: [
 | tactic_value
 | Constr.constr

diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
@@ -2204,8 +2204,6 @@ ltac_expr2: [
 ]
 
 ltac_expr1: [
-| "fun" LIST1 name "=>" ltac_expr
-| "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr
 | tactic_value
 | qualid LIST1 tactic_arg
 | l1_tactic

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;
 
@@ -128,7 +128,11 @@ GRAMMAR EXTEND Gram
               "else" ; tae = ltac_expr -> { CAst.make ~loc (TacIfThenCatch (ta,tat,tae)) }
       | ta0 = ltac_expr; "||"; ta1 = ltac_expr -> { CAst.make ~loc (TacOrelse (ta0,ta1)) } ]
     | "1" RIGHTA
-      [ te = binder_tactic -> { te }
+      [ "fun"; it = LIST1 input_fun ; "=>"; body = ltac_expr LEVEL "5" ->
+          { CAst.make ~loc (TacFun (it,body)) }
+      | "let"; isrec = [IDENT "rec" -> { true } | -> { false } ];
+          llc = LIST1 let_clause SEP "with"; "in";
+          body = ltac_expr LEVEL "5" -> { CAst.make ~loc (TacLetIn (isrec,llc,body)) }
       | b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
           { CAst.make ~loc (TacMatchGoal (b,false,mrl)) }
       | b = match_key; IDENT "reverse"; IDENT "goal"; "with";
@@ -160,15 +164,6 @@ GRAMMAR EXTEND Gram
   failkw:
   [ [ IDENT "fail" -> { TacLocal } | IDENT "gfail" -> { TacGlobal } ] ]
   ;
-  (* binder_tactic: level 1 of ltac_expr *)
-  binder_tactic:
-    [ RIGHTA
-      [ "fun"; it = LIST1 input_fun ; "=>"; body = ltac_expr LEVEL "5" ->
-          { CAst.make ~loc (TacFun (it,body)) }
-      | "let"; isrec = [IDENT "rec" -> { true } | -> { false } ];
-          llc = LIST1 let_clause SEP "with"; "in";
-          body = ltac_expr LEVEL "5" -> { CAst.make ~loc (TacLetIn (isrec,llc,body)) } ] ]
-  ;
   (* 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
@@ -32,8 +32,7 @@ type argument = Genarg.ArgT.any Extend.user_symbol
 (* Interpret entry names of the form "ne_constr_list" as entry keys   *)
 
 let atactic n =
-  if n = 5 then Pcoq.Symbol.nterm Pltac.binder_tactic
-  else Pcoq.Symbol.nterml Pltac.ltac_expr (string_of_int n)
+  Pcoq.Symbol.nterml Pltac.ltac_expr (string_of_int n)
 
 type entry_name = EntryName :
   'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.Symbol.t -> entry_name
@@ -42,7 +41,6 @@ type entry_name = EntryName :
 let get_tacentry n m =
   let check_lvl n =
     Int.equal m n
-    && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
     && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
   in
   if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Pcoq.Symbol.self)
@@ -113,9 +111,7 @@ let interp_entry_name interp symb =
 let get_tactic_entry n =
   if Int.equal n 0 then
     Pltac.simple_tactic, None
-  else if Int.equal n 5 then
-    Pltac.binder_tactic, None
-  else if 1<=n && n<5 then
+  else if 1<=n && n<=5 then
     Pltac.ltac_expr, Some (string_of_int n)
   else
     user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^"."))
@@ -624,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

diff --git a/test-suite/output/bug_18368.out b/test-suite/output/bug_18368.out
@@ -0,0 +1 @@
+B
diff --git a/test-suite/output/bug_18368.v b/test-suite/output/bug_18368.v
@@ -0,0 +1,6 @@
+Tactic Notation (at level 4) "test" := idtac "A".
+Tactic Notation (at level 5) "test" := idtac "B".
+
+Goal True.
+test.
+Abort.