diff options
| author | coqbot-app[bot] | 2020-10-27 21:12:37 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-27 21:12:37 +0000 |
| commit | c8110e13cceab22dd855de7ee2114bcb4eedd699 (patch) | |
| tree | 9fa2c8f1922075942998828523137debf9bf0c1e | |
| parent | 96354508a50f12a2af49bd95073c6a24cea69713 (diff) | |
| parent | 480d34fc22c195d4b19f639345fa993652838894 (diff) | |
Merge PR #13219: Rename mlg grammar nonterminals to make documented and mlg grammars more consistent
Reviewed-by: Zimmi48
Reviewed-by: herbelin
Ack-by: SkySkimmer
39 files changed, 863 insertions, 925 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 5e3199e8a6..83929bd030 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -469,7 +469,7 @@ let rec parse_symb self = function | Uentryl (e, l) -> assert (e = "tactic"); if l = 5 then SymbEntry ("Pltac.binder_tactic", None) - else SymbEntry ("Pltac.tactic_expr", Some (string_of_int l)) + else SymbEntry ("Pltac.ltac_expr", Some (string_of_int l)) let parse_token self = function | ExtTerminal s -> (terminal s, None) diff --git a/dev/doc/parsing.md b/dev/doc/parsing.md index 4982e3e94d..4956b91d01 100644 --- a/dev/doc/parsing.md +++ b/dev/doc/parsing.md @@ -210,7 +210,7 @@ command. The first square bracket around a nonterminal definition is for groupi level definitions, which are separated with `|`, for example: ``` - tactic_expr: + ltac_expr: [ "5" RIGHTA [ te = binder_tactic -> { te } ] | "4" LEFTA @@ -220,8 +220,8 @@ level definitions, which are separated with `|`, for example: Grammar extensions can specify what level they are modifying, for example: ``` - tactic_expr: LEVEL "1" [ RIGHTA - [ tac = tactic_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros } + ltac_expr: LEVEL "1" [ RIGHTA + [ tac = ltac_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros } ] ]; ``` diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 122b0f5dfb..ba0ec28f8b 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -342,9 +342,9 @@ Recursive functions: fix .. insertprodn term_fix fixannot .. prodn:: - term_fix ::= let fix @fix_body in @term - | fix @fix_body {? {+ with @fix_body } for @ident } - fix_body ::= @ident {* @binder } {? @fixannot } {? : @type } := @term + term_fix ::= let fix @fix_decl in @term + | fix @fix_decl {? {+ with @fix_decl } for @ident } + fix_decl ::= @ident {* @binder } {? @fixannot } {? : @type } := @term fixannot ::= %{ struct @ident %} | %{ wf @one_term @ident %} | %{ measure @one_term {? @ident } {? @one_term } %} diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 5c091f04ac..8663ac646b 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -161,7 +161,7 @@ Syntactic values Provides a way to use the syntax and semantics of a grammar nonterminal as a value in an :token:`ltac_expr`. The table below describes the most useful of these. You can see the others by running ":cmd:`Print Grammar` `tactic`" and -examining the part at the end under "Entry tactic:tactic_arg". +examining the part at the end under "Entry tactic:tactic_value". :token:`ident` name of a grammar nonterminal listed in the table diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 770de9a6c3..cdbae8ade1 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -5724,11 +5724,11 @@ respectively. local function definition -.. tacv:: pose fix @fix_body +.. tacv:: pose fix @fix_decl local fix definition -.. tacv:: pose cofix @fix_body +.. tacv:: pose cofix @fix_decl local cofix definition diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 0c51361b64..06018304ab 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -444,7 +444,7 @@ Displaying information about notations This command doesn't display all nonterminals of the grammar. For example, productions shown by `Print Grammar tactic` refer to nonterminals `tactic_then_locality` - and `tactic_then_gen` which are not shown and can't be printed. + and `for_each_goal` which are not shown and can't be printed. Most of the grammar in the documentation was updated in 8.12 to make it accurate and readable. This was done using a new developer tool that extracts the grammar from the @@ -477,16 +477,16 @@ Displaying information about notations such as `1+2*3` in the usual way as `1+(2*3)`. However, most nonterminals have a single level. For example, this output from `Print Grammar tactic` shows the first 3 levels for - `tactic_expr`, designated as "5", "4" and "3". Level 3 is right-associative, + `ltac_expr`, designated as "5", "4" and "3". Level 3 is right-associative, which applies to the productions within it, such as the `try` construct:: - Entry tactic_expr is + Entry ltac_expr is [ "5" RIGHTA [ binder_tactic ] | "4" LEFTA [ SELF; ";"; binder_tactic | SELF; ";"; SELF - | SELF; ";"; tactic_then_locality; tactic_then_gen; "]" ] + | SELF; ";"; tactic_then_locality; for_each_goal; "]" ] | "3" RIGHTA [ IDENT "try"; SELF : @@ -510,7 +510,7 @@ Displaying information about notations The output for `Print Grammar constr` includes :cmd:`Notation` definitions, which are dynamically added to the grammar at run time. - For example, in the definition for `operconstr`, the production on the second line shown + For example, in the definition for `term`, the production on the second line shown here is defined by a :cmd:`Reserved Notation` command in `Notations.v`:: | "50" LEFTA diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md index 4d38955fa8..dbb04bb6a6 100644 --- a/doc/tools/docgram/README.md +++ b/doc/tools/docgram/README.md @@ -42,7 +42,7 @@ for documentation purposes: First, nonterminals that use levels (`"5" RIGHTA` below) are modified, for example: ``` - tactic_expr: + ltac_expr: [ "5" RIGHTA [ te = binder_tactic -> { te } ] [ "4" ... diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index f9aba5b1e1..f6a684bbd7 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -28,15 +28,15 @@ strategy_level_or_var: [ | strategy_level ] -operconstr0: [ -| "ltac" ":" "(" tactic_expr5 ")" +term0: [ +| "ltac" ":" "(" ltac_expr5 ")" ] EXTRAARGS_natural: [ | DELETENT ] EXTRAARGS_lconstr: [ | DELETENT ] EXTRAARGS_strategy_level: [ | DELETENT ] G_LTAC_hint: [ | DELETENT ] -G_LTAC_operconstr0: [ | DELETENT ] +G_LTAC_term0: [ | DELETENT ] G_REWRITE_binders: [ | DELETE Pcoq.Constr.binders @@ -86,7 +86,7 @@ RENAME: [ | G_LTAC2_eqn_ipat ltac2_eqn_ipat | G_LTAC2_conversion ltac2_conversion | G_LTAC2_oriented_rewriter ltac2_oriented_rewriter -| G_LTAC2_tactic_then_gen ltac2_tactic_then_gen +| G_LTAC2_for_each_goal ltac2_for_each_goal | G_LTAC2_tactic_then_last ltac2_tactic_then_last | G_LTAC2_as_name ltac2_as_name | G_LTAC2_as_ipat ltac2_as_ipat @@ -94,18 +94,22 @@ RENAME: [ | G_LTAC2_match_list ltac2_match_list ] -(* renames to eliminate qualified names - put other renames at the end *) +(* Renames to eliminate qualified names. + Put other renames at the end *) RENAME: [ (* map missing names for rhs *) | Constr.constr term | Constr.global global | Constr.lconstr lconstr -| Constr.lconstr_pattern cpattern +| Constr.cpattern cpattern | G_vernac.query_command query_command | G_vernac.section_subset_expr section_var_expr | Prim.ident ident | Prim.reference reference +| Prim.string string +| Prim.integer integer +| Prim.qualid qualid +| Prim.natural natural | Pvernac.Vernac_.main_entry vernac_control | Tactic.tactic tactic @@ -117,7 +121,7 @@ RENAME: [ | Prim.identref ident | Prim.natural natural *) -| Vernac.rec_definition rec_definition +| Vernac.fix_definition fix_definition (* todo: hmm, rename adds 1 prodn to closed_binder?? *) | Constr.closed_binder closed_binder ] @@ -183,19 +187,19 @@ DELETE: [ (* additional nts to be spliced *) tactic_then_last: [ -| REPLACE "|" LIST0 ( OPT tactic_expr5 ) SEP "|" -| WITH LIST0 ( "|" ( OPT tactic_expr5 ) ) +| REPLACE "|" LIST0 ( OPT ltac_expr5 ) SEP "|" +| WITH LIST0 ( "|" ( OPT ltac_expr5 ) ) ] goal_tactics: [ -| LIST0 ( OPT tactic_expr5 ) SEP "|" +| LIST0 ( OPT ltac_expr5 ) SEP "|" ] -tactic_then_gen: [ | DELETENT ] +for_each_goal: [ | DELETENT ] -tactic_then_gen: [ +for_each_goal: [ | goal_tactics -| OPT ( goal_tactics "|" ) OPT tactic_expr5 ".." OPT ( "|" goal_tactics ) +| OPT ( goal_tactics "|" ) OPT ltac_expr5 ".." OPT ( "|" goal_tactics ) ] tactic_then_last: [ @@ -203,19 +207,19 @@ tactic_then_last: [ ] ltac2_tactic_then_last: [ -| REPLACE "|" LIST0 ( OPT tac2expr6 ) SEP "|" (* Ltac2 plugin *) -| WITH LIST0 ( "|" OPT tac2expr6 ) TAG Ltac2 +| REPLACE "|" LIST0 ( OPT ltac2_expr6 ) SEP "|" (* Ltac2 plugin *) +| WITH LIST0 ( "|" OPT ltac2_expr6 ) TAG Ltac2 ] ltac2_goal_tactics: [ -| LIST0 ( OPT tac2expr6 ) SEP "|" TAG Ltac2 +| LIST0 ( OPT ltac2_expr6 ) SEP "|" TAG Ltac2 ] -ltac2_tactic_then_gen: [ | DELETENT ] +ltac2_for_each_goal: [ | DELETENT ] -ltac2_tactic_then_gen: [ +ltac2_for_each_goal: [ | ltac2_goal_tactics TAG Ltac2 -| OPT ( ltac2_goal_tactics "|" ) OPT tac2expr6 ".." OPT ( "|" ltac2_goal_tactics ) TAG Ltac2 +| OPT ( ltac2_goal_tactics "|" ) OPT ltac2_expr6 ".." OPT ( "|" ltac2_goal_tactics ) TAG Ltac2 ] ltac2_tactic_then_last: [ @@ -257,45 +261,40 @@ let_type_cstr: [ | type_cstr ] -(* rename here because we want to use "return_type" for something else *) -RENAME: [ -| return_type as_return_type -] - case_item: [ -| REPLACE operconstr100 OPT [ "as" name ] OPT [ "in" pattern200 ] -| WITH operconstr100 OPT ("as" name) OPT [ "in" pattern200 ] +| REPLACE term100 OPT [ "as" name ] OPT [ "in" pattern200 ] +| WITH term100 OPT ("as" name) OPT [ "in" pattern200 ] ] binder_constr: [ -| MOVETO term_forall_or_fun "forall" open_binders "," operconstr200 -| MOVETO term_forall_or_fun "fun" open_binders "=>" operconstr200 -| MOVETO term_let "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200 -| MOVETO term_if "if" operconstr200 as_return_type "then" operconstr200 "else" operconstr200 -| MOVETO term_fix "let" "fix" fix_decl "in" operconstr200 -| MOVETO term_cofix "let" "cofix" cofix_decl "in" operconstr200 -| MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" operconstr200 "in" operconstr200 -| MOVETO term_let "let" "'" pattern200 ":=" operconstr200 "in" operconstr200 -| MOVETO term_let "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200 -| MOVETO term_let "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200 +| MOVETO term_forall_or_fun "forall" open_binders "," term200 +| MOVETO term_forall_or_fun "fun" open_binders "=>" term200 +| MOVETO term_let "let" name binders let_type_cstr ":=" term200 "in" term200 +| MOVETO term_if "if" term200 as_return_type "then" term200 "else" term200 +| MOVETO term_fix "let" "fix" fix_decl "in" term200 +| MOVETO term_cofix "let" "cofix" cofix_body "in" term200 +| MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200 +| MOVETO term_let "let" "'" pattern200 ":=" term200 "in" term200 +| MOVETO term_let "let" "'" pattern200 ":=" term200 case_type "in" term200 +| MOVETO term_let "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200 | MOVETO term_fix "fix" fix_decls | MOVETO term_cofix "cofix" cofix_decls ] term_let: [ -| REPLACE "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200 -| WITH "let" name let_type_cstr ":=" operconstr200 "in" operconstr200 -| "let" name LIST1 binder let_type_cstr ":=" operconstr200 "in" operconstr200 +| REPLACE "let" name binders let_type_cstr ":=" term200 "in" term200 +| WITH "let" name let_type_cstr ":=" term200 "in" term200 +| "let" name LIST1 binder let_type_cstr ":=" term200 "in" term200 (* Don't need to document that "( )" is equivalent to "()" *) -| REPLACE "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" operconstr200 "in" operconstr200 -| WITH "let" "(" LIST0 name SEP "," ")" as_return_type ":=" operconstr200 "in" operconstr200 -| REPLACE "let" "'" pattern200 ":=" operconstr200 "in" operconstr200 -| WITH "let" "'" pattern200 ":=" operconstr200 OPT case_type "in" operconstr200 -| DELETE "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200 +| REPLACE "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200 +| WITH "let" "(" LIST0 name SEP "," ")" as_return_type ":=" term200 "in" term200 +| REPLACE "let" "'" pattern200 ":=" term200 "in" term200 +| WITH "let" "'" pattern200 ":=" term200 OPT case_type "in" term200 +| DELETE "let" "'" pattern200 ":=" term200 case_type "in" term200 ] atomic_constr: [ -| MOVETO qualid_annotated global univ_instance +| MOVETO qualid_annotated global univ_annot | MOVETO primitive_notations NUMBER | MOVETO primitive_notations string | MOVETO term_evar "_" @@ -308,9 +307,9 @@ atomic_constr: [ | MOVETO term_evar pattern_ident evar_instance ] -tactic_expr0: [ -| REPLACE "[" ">" tactic_then_gen "]" -| WITH "[>" tactic_then_gen "]" +ltac_expr0: [ +| REPLACE "[" ">" for_each_goal "]" +| WITH "[>" for_each_goal "]" ] (* lexer token *) @@ -337,68 +336,68 @@ scope_delimiter: [ ] type: [ -| operconstr200 +| term200 ] -operconstr100: [ -| REPLACE operconstr99 "<:" operconstr200 -| WITH operconstr99 "<:" type -| MOVETO term_cast operconstr99 "<:" type -| REPLACE operconstr99 "<<:" operconstr200 -| WITH operconstr99 "<<:" type -| MOVETO term_cast operconstr99 "<<:" type -| REPLACE operconstr99 ":" operconstr200 -| WITH operconstr99 ":" type -| MOVETO term_cast operconstr99 ":" type -| MOVETO term_cast operconstr99 ":>" +term100: [ +| REPLACE term99 "<:" term200 +| WITH term99 "<:" type +| MOVETO term_cast term99 "<:" type +| REPLACE term99 "<<:" term200 +| WITH term99 "<<:" type +| MOVETO term_cast term99 "<<:" type +| REPLACE term99 ":" term200 +| WITH term99 ":" type +| MOVETO term_cast term99 ":" type +| MOVETO term_cast term99 ":>" ] constr: [ -| REPLACE "@" global univ_instance +| REPLACE "@" global univ_annot | WITH "@" qualid_annotated | MOVETO term_explicit "@" qualid_annotated ] -operconstr10: [ +term10: [ (* Separate this LIST0 in the nonempty and the empty case *) (* The empty case is covered by constr *) -| REPLACE "@" global univ_instance LIST0 operconstr9 -| WITH "@" qualid_annotated LIST1 operconstr9 -| REPLACE operconstr9 +| REPLACE "@" global univ_annot LIST0 term9 +| WITH "@" qualid_annotated LIST1 term9 +| REPLACE term9 | WITH constr -| MOVETO term_application operconstr9 LIST1 appl_arg -| MOVETO term_application "@" qualid_annotated LIST1 operconstr9 +| MOVETO term_application term9 LIST1 arg +| MOVETO term_application "@" qualid_annotated LIST1 term9 (* fixme: add in as a prodn somewhere *) | MOVETO dangling_pattern_extension_rule "@" pattern_ident LIST1 identref | DELETE dangling_pattern_extension_rule ] -operconstr9: [ +term9: [ (* @Zimmi48: Special token .. is for use in the Notation command. (see bug_3304.v) *) -| DELETE ".." operconstr0 ".." +| DELETE ".." term0 ".." ] -operconstr1: [ -| REPLACE operconstr0 ".(" global LIST0 appl_arg ")" -| WITH operconstr0 ".(" global LIST0 appl_arg ")" (* huh? *) -| REPLACE operconstr0 "%" IDENT -| WITH operconstr0 "%" scope_key -| MOVETO term_scope operconstr0 "%" scope_key -| MOVETO term_projection operconstr0 ".(" global LIST0 appl_arg ")" -| MOVETO term_projection operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")" +term1: [ +| REPLACE term0 ".(" global LIST0 arg ")" +| WITH term0 ".(" global LIST0 arg ")" (* huh? *) +| REPLACE term0 "%" IDENT +| WITH term0 "%" scope_key +| MOVETO term_scope term0 "%" scope_key +| MOVETO term_projection term0 ".(" global LIST0 arg ")" +| MOVETO term_projection term0 ".(" "@" global LIST0 ( term9 ) ")" ] -operconstr0: [ +term0: [ (* @Zimmi48: This rule is a hack, according to Hugo, and should not be shown in the manual. *) | DELETE "{" binder_constr "}" | REPLACE "{|" record_declaration bar_cbrace | WITH "{|" LIST0 field_def SEP ";" OPT ";" bar_cbrace | MOVETO term_record "{|" LIST0 field_def SEP ";" OPT ";" bar_cbrace -| MOVETO term_generalizing "`{" operconstr200 "}" -| MOVETO term_generalizing "`(" operconstr200 ")" -| MOVETO term_ltac "ltac" ":" "(" tactic_expr5 ")" -| REPLACE "[" "|" array_elems "|" lconstr type_cstr "|" "]" univ_instance -| WITH "[|" array_elems "|" lconstr type_cstr "|]" univ_instance +| MOVETO term_generalizing "`{" term200 "}" +| MOVETO term_generalizing "`(" term200 ")" +| MOVETO term_ltac "ltac" ":" "(" ltac_expr5 ")" +| REPLACE "[" "|" array_elems "|" lconstr type_cstr "|" "]" univ_annot +| WITH "[|" array_elems "|" lconstr type_cstr "|]" univ_annot ] fix_decls: [ @@ -408,9 +407,9 @@ fix_decls: [ ] cofix_decls: [ -| DELETE cofix_decl -| REPLACE cofix_decl "with" LIST1 cofix_decl SEP "with" "for" identref -| WITH cofix_decl OPT ( LIST1 ( "with" cofix_decl ) "for" identref ) +| DELETE cofix_body +| REPLACE cofix_body "with" LIST1 cofix_body SEP "with" "for" identref +| WITH cofix_body OPT ( LIST1 ( "with" cofix_body ) "for" identref ) ] fields_def: [ @@ -481,11 +480,11 @@ name_colon: [ ] typeclass_constraint: [ -| EDIT ADD_OPT "!" operconstr200 -| REPLACE "{" name "}" ":" [ "!" | ] operconstr200 -| WITH "{" name "}" ":" OPT "!" operconstr200 -| REPLACE name ":" [ "!" | ] operconstr200 -| WITH name ":" OPT "!" operconstr200 +| EDIT ADD_OPT "!" term200 +| REPLACE "{" name "}" ":" [ "!" | ] term200 +| WITH "{" name "}" ":" OPT "!" term200 +| REPLACE name ":" [ "!" | ] term200 +| WITH name ":" OPT "!" term200 ] (* ?? From the grammar, Prim.name seems to be only "_" but ident is also accepted "*) @@ -566,14 +565,14 @@ gallina: [ | [ "Record" | "Structure" ] record_definition LIST0 ( "with" record_definition ) | "Class" record_definition | "Class" singleton_class_definition -| REPLACE "Fixpoint" LIST1 rec_definition SEP "with" -| WITH "Fixpoint" rec_definition LIST0 ( "with" rec_definition ) -| REPLACE "Let" "Fixpoint" LIST1 rec_definition SEP "with" -| WITH "Let" "Fixpoint" rec_definition LIST0 ( "with" rec_definition ) -| REPLACE "CoFixpoint" LIST1 corec_definition SEP "with" -| WITH "CoFixpoint" corec_definition LIST0 ( "with" corec_definition ) -| REPLACE "Let" "CoFixpoint" LIST1 corec_definition SEP "with" -| WITH "Let" "CoFixpoint" corec_definition LIST0 ( "with" corec_definition ) +| REPLACE "Fixpoint" LIST1 fix_definition SEP "with" +| WITH "Fixpoint" fix_definition LIST0 ( "with" fix_definition ) +| REPLACE "Let" "Fixpoint" LIST1 fix_definition SEP "with" +| WITH "Let" "Fixpoint" fix_definition LIST0 ( "with" fix_definition ) +| REPLACE "CoFixpoint" LIST1 cofix_definition SEP "with" +| WITH "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition ) +| REPLACE "Let" "CoFixpoint" LIST1 cofix_definition SEP "with" +| WITH "Let" "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition ) | REPLACE "Scheme" LIST1 scheme SEP "with" | WITH "Scheme" scheme LIST0 ( "with" scheme ) ] @@ -582,7 +581,7 @@ finite_token: [ | DELETENT ] -constructor_list_or_record_decl: [ +constructors_or_record: [ | OPTINREF ] @@ -604,7 +603,7 @@ inline: [ | OPTINREF ] -univ_instance: [ +univ_annot: [ | OPTINREF ] @@ -613,15 +612,15 @@ univ_decl: [ | WITH "@{" LIST0 identref OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}" ] -of_type_with_opt_coercion: [ +of_type: [ | DELETENT ] -of_type_with_opt_coercion: [ +of_type: [ | [ ":" | ":>" ] type ] -attribute_value: [ +attr_value: [ | OPTINREF ] @@ -657,14 +656,6 @@ ltac2_branches: [ | OPTINREF ] -RENAME: [ -| red_flag ltac2_red_flag -| red_flags red_flag -] - -RENAME: [ -] - strategy_flag: [ | REPLACE OPT delta_flag | WITH delta_flag @@ -697,8 +688,8 @@ is_module_type: [ ] gallina_ext: [ -| REPLACE "Arguments" smart_global LIST0 argument_spec_block OPT [ "," LIST1 [ LIST0 more_implicits_block ] SEP "," ] OPT [ ":" LIST1 arguments_modifier SEP "," ] -| WITH "Arguments" smart_global LIST0 argument_spec_block LIST0 [ "," LIST0 more_implicits_block ] OPT [ ":" LIST1 arguments_modifier SEP "," ] +| REPLACE "Arguments" smart_global LIST0 arg_specs OPT [ "," LIST1 [ LIST0 implicits_alt ] SEP "," ] OPT [ ":" LIST1 args_modifier SEP "," ] +| WITH "Arguments" smart_global LIST0 arg_specs LIST0 [ "," LIST0 implicits_alt ] OPT [ ":" LIST1 args_modifier SEP "," ] | REPLACE "Implicit" "Type" reserv_list | WITH "Implicit" [ "Type" | "Types" ] reserv_list | DELETE "Implicit" "Types" reserv_list @@ -727,11 +718,11 @@ gallina_ext: [ | WITH "Generalizable" [ [ "Variable" | "Variables" ] LIST1 identref | "All" "Variables" | "No" "Variables" ] (* don't show Export for Set, Unset *) -| REPLACE "Export" "Set" option_table option_setting -| WITH "Set" option_table option_setting -| REPLACE "Export" "Unset" option_table -| WITH "Unset" option_table -| REPLACE "Instance" instance_name ":" operconstr200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ] +| REPLACE "Export" "Set" setting_name option_setting +| WITH "Set" setting_name option_setting +| REPLACE "Export" "Unset" setting_name +| WITH "Unset" setting_name +| REPLACE "Instance" instance_name ":" term200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ] | WITH "Instance" instance_name ":" type hint_info OPT [ ":=" "{" record_declaration "}" | ":=" lconstr ] | REPLACE "From" global "Require" export_token LIST1 global @@ -822,92 +813,92 @@ DELETE: [ | tactic_then_locality ] -tactic_expr5: [ -(* make these look consistent with use of binder_tactic in other tactic_expr* *) +ltac_expr5: [ +(* make these look consistent with use of binder_tactic in other ltac_expr* *) | DELETE binder_tactic -| DELETE tactic_expr4 -| [ tactic_expr4 | binder_tactic ] +| DELETE ltac_expr4 +| [ ltac_expr4 | binder_tactic ] ] ltac_constructs: [ (* repeated in main ltac grammar - need to create a COPY edit *) -| tactic_expr3 ";" [ tactic_expr3 | binder_tactic ] -| tactic_expr3 ";" "[" tactic_then_gen "]" +| ltac_expr3 ";" [ ltac_expr3 | binder_tactic ] +| ltac_expr3 ";" "[" for_each_goal "]" -| tactic_expr1 "+" [ tactic_expr2 | binder_tactic ] -| tactic_expr1 "||" [ tactic_expr2 | binder_tactic ] +| ltac_expr1 "+" [ ltac_expr2 | binder_tactic ] +| ltac_expr1 "||" [ ltac_expr2 | binder_tactic ] -(* | qualid LIST0 tactic_arg add later due renaming tactic_arg *) +(* | qualid LIST0 tactic_value add later due renaming tactic_value *) -| "[>" tactic_then_gen "]" -| toplevel_selector tactic_expr5 +| "[>" for_each_goal "]" +| toplevel_selector ltac_expr5 ] -tactic_expr4: [ -| REPLACE tactic_expr3 ";" tactic_then_gen "]" -| WITH tactic_expr3 ";" "[" tactic_then_gen "]" -| REPLACE tactic_expr3 ";" binder_tactic -| WITH tactic_expr3 ";" [ tactic_expr3 | binder_tactic ] -| DELETE tactic_expr3 ";" tactic_expr3 +ltac_expr4: [ +| REPLACE ltac_expr3 ";" for_each_goal "]" +| WITH ltac_expr3 ";" "[" for_each_goal "]" +| REPLACE ltac_expr3 ";" binder_tactic +| WITH ltac_expr3 ";" [ ltac_expr3 | binder_tactic ] +| DELETE ltac_expr3 ";" ltac_expr3 ] l3_tactic: [ ] -tactic_expr3: [ -| DELETE "abstract" tactic_expr2 -| REPLACE "abstract" tactic_expr2 "using" ident -| WITH "abstract" tactic_expr2 OPT ( "using" ident ) +ltac_expr3: [ +| DELETE "abstract" ltac_expr2 +| REPLACE "abstract" ltac_expr2 "using" ident +| WITH "abstract" ltac_expr2 OPT ( "using" ident ) | l3_tactic | MOVEALLBUT ltac_builtins | l3_tactic -| tactic_expr2 +| ltac_expr2 ] l2_tactic: [ ] -tactic_expr2: [ -| REPLACE tactic_expr1 "+" binder_tactic -| WITH tactic_expr1 "+" [ tactic_expr2 | binder_tactic ] -| DELETE tactic_expr1 "+" tactic_expr2 -| REPLACE tactic_expr1 "||" binder_tactic -| WITH tactic_expr1 "||" [ tactic_expr2 | binder_tactic ] -| DELETE tactic_expr1 "||" tactic_expr2 -| MOVETO ltac_builtins "tryif" tactic_expr5 "then" tactic_expr5 "else" tactic_expr2 +ltac_expr2: [ +| REPLACE ltac_expr1 "+" binder_tactic +| WITH ltac_expr1 "+" [ ltac_expr2 | binder_tactic ] +| DELETE ltac_expr1 "+" ltac_expr2 +| REPLACE ltac_expr1 "||" binder_tactic +| WITH ltac_expr1 "||" [ ltac_expr2 | binder_tactic ] +| DELETE ltac_expr1 "||" ltac_expr2 +| MOVETO ltac_builtins "tryif" ltac_expr5 "then" ltac_expr5 "else" ltac_expr2 | l2_tactic | DELETE ltac_builtins ] l1_tactic: [ ] -tactic_expr1: [ +ltac_expr1: [ | 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 tactic_expr5 "with" match_list "end" +| MOVETO simple_tactic match_key ltac_expr5 "with" match_list "end" | REPLACE failkw [ int_or_var | ] LIST0 message_token | WITH failkw OPT int_or_var LIST0 message_token -| REPLACE reference LIST0 tactic_arg_compat -| WITH reference LIST1 tactic_arg_compat +| REPLACE reference LIST0 tactic_arg +| WITH reference LIST1 tactic_arg | l1_tactic | DELETE simple_tactic | MOVEALLBUT ltac_builtins | l1_tactic -| tactic_arg -| reference LIST1 tactic_arg_compat -| tactic_expr0 +| tactic_value +| reference LIST1 tactic_arg +| ltac_expr0 ] (* split match_context_rule *) goal_pattern: [ -| LIST0 match_hyps SEP "," "|-" match_pattern -| "[" LIST0 match_hyps SEP "," "|-" match_pattern "]" +| LIST0 match_hyp SEP "," "|-" match_pattern +| "[" LIST0 match_hyp SEP "," "|-" match_pattern "]" | "_" ] match_context_rule: [ -| DELETE LIST0 match_hyps SEP "," "|-" match_pattern "=>" tactic_expr5 -| DELETE "[" LIST0 match_hyps SEP "," "|-" match_pattern "]" "=>" tactic_expr5 -| DELETE "_" "=>" tactic_expr5 -| goal_pattern "=>" tactic_expr5 +| DELETE LIST0 match_hyp SEP "," "|-" match_pattern "=>" ltac_expr5 +| DELETE "[" LIST0 match_hyp SEP "," "|-" match_pattern "]" "=>" ltac_expr5 +| DELETE "_" "=>" ltac_expr5 +| goal_pattern "=>" ltac_expr5 ] match_context_list: [ @@ -920,10 +911,10 @@ match_list: [ match_rule: [ (* redundant; match_pattern -> term -> _ *) -| DELETE "_" "=>" tactic_expr5 +| DELETE "_" "=>" ltac_expr5 ] -selector_body: [ +selector: [ | REPLACE range_selector_or_nth (* depends on whether range_selector_or_nth is deleted first *) | WITH LIST1 range_selector SEP "," ] @@ -1091,7 +1082,7 @@ simple_tactic: [ | EDIT "psatz_Q" ADD_OPT int_or_var tactic | EDIT "psatz_Z" ADD_OPT int_or_var tactic | REPLACE "subst" LIST1 hyp -| WITH "subst" OPT ( LIST1 hyp ) +| WITH "subst" LIST0 hyp | DELETE "subst" | DELETE "congruence" | DELETE "congruence" natural @@ -1102,18 +1093,18 @@ simple_tactic: [ | REPLACE "show" "ltac" "profile" "cutoff" integer | WITH "show" "ltac" "profile" OPT [ "cutoff" integer | string ] | DELETE "show" "ltac" "profile" string -(* perversely, the mlg uses "tactic3" instead of "tactic_expr3" *) +(* perversely, the mlg uses "tactic3" instead of "ltac_expr3" *) | DELETE "transparent_abstract" tactic3 | REPLACE "transparent_abstract" tactic3 "using" ident -| WITH "transparent_abstract" tactic_expr3 OPT ( "using" ident ) -| REPLACE "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 preident -| WITH "typeclasses" "eauto" OPT "bfs" OPT int_or_var OPT ( "with" LIST1 preident ) +| WITH "transparent_abstract" ltac_expr3 OPT ( "using" ident ) +| "typeclasses" "eauto" OPT "bfs" OPT int_or_var OPT ( "with" LIST1 preident ) +| DELETE "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 preident | DELETE "typeclasses" "eauto" OPT int_or_var "with" LIST1 preident | DELETE "typeclasses" "eauto" "bfs" OPT int_or_var | DELETE "typeclasses" "eauto" OPT int_or_var (* in Tactic Notation: *) | "setoid_replace" constr "with" constr OPT ( "using" "relation" constr ) OPT ( "in" hyp ) - OPT ( "at" LIST1 int_or_var ) OPT ( "by" tactic_expr3 ) + OPT ( "at" LIST1 int_or_var ) OPT ( "by" ltac_expr3 ) ] (* todo: don't use DELETENT for this *) @@ -1168,8 +1159,8 @@ command: [ | "SubClass" ident_decl def_body | REPLACE "Ltac" LIST1 ltac_tacdef_body SEP "with" | WITH "Ltac" ltac_tacdef_body LIST0 ( "with" ltac_tacdef_body ) -| REPLACE "Function" LIST1 function_rec_definition_loc SEP "with" (* funind plugin *) -| WITH "Function" function_rec_definition_loc LIST0 ( "with" function_rec_definition_loc ) (* funind plugin *) +| REPLACE "Function" LIST1 function_fix_definition SEP "with" (* funind plugin *) +| WITH "Function" function_fix_definition LIST0 ( "with" function_fix_definition ) (* funind plugin *) | REPLACE "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with" (* funind plugin *) | WITH "Functional" "Scheme" fun_scheme_arg LIST0 ( "with" fun_scheme_arg ) (* funind plugin *) | DELETE "Cd" @@ -1180,16 +1171,16 @@ command: [ | WITH "Back" OPT natural | REPLACE "Load" [ "Verbose" | ] [ ne_string | IDENT ] | WITH "Load" OPT "Verbose" [ ne_string | IDENT ] -| DELETE "Unset" option_table -| REPLACE "Set" option_table option_setting -| WITH OPT "Export" "Set" option_table (* set flag *) -| REPLACE "Test" option_table "for" LIST1 table_value -| WITH "Test" option_table OPT ( "for" LIST1 table_value ) -| DELETE "Test" option_table +| DELETE "Unset" setting_name +| REPLACE "Set" setting_name option_setting +| WITH OPT "Export" "Set" setting_name (* set flag *) +| REPLACE "Test" setting_name "for" LIST1 table_value +| WITH "Test" setting_name OPT ( "for" LIST1 table_value ) +| DELETE "Test" setting_name (* hide the fact that table names are limited to 2 IDENTs *) | REPLACE "Add" IDENT IDENT LIST1 table_value -| WITH "Add" option_table LIST1 table_value +| WITH "Add" setting_name LIST1 table_value | DELETE "Add" IDENT LIST1 table_value | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident @@ -1247,7 +1238,7 @@ command: [ (* hide the fact that table names are limited to 2 IDENTs *) | REPLACE "Remove" IDENT IDENT LIST1 table_value -| WITH "Remove" option_table LIST1 table_value +| WITH "Remove" setting_name LIST1 table_value | DELETE "Remove" IDENT LIST1 table_value | DELETE "Restore" "State" IDENT | DELETE "Restore" "State" ne_string @@ -1294,10 +1285,10 @@ command: [ | WITH "Declare" "Scope" scope_name (* odd that these are in command while other notation-related ones are in syntax *) -| REPLACE "Numeral" "Notation" reference reference reference ":" ident numnotoption -| WITH "Numeral" "Notation" reference reference reference ":" scope_name numnotoption -| REPLACE "Number" "Notation" reference reference reference ":" ident numnotoption -| WITH "Number" "Notation" reference reference reference ":" scope_name numnotoption +| REPLACE "Numeral" "Notation" reference reference reference ":" ident numeral_modifier +| WITH "Numeral" "Notation" reference reference reference ":" scope_name numeral_modifier +| REPLACE "Number" "Notation" reference reference reference ":" ident numeral_modifier +| WITH "Number" "Notation" reference reference reference ":" scope_name numeral_modifier | REPLACE "String" "Notation" reference reference reference ":" ident | WITH "String" "Notation" reference reference reference ":" scope_name @@ -1357,7 +1348,7 @@ syntax_modifier: [ | WITH LIST1 IDENT SEP "," "at" level ] -syntax_extension_type: [ +explicit_subentry: [ | REPLACE "strict" "pattern" "at" "level" natural | WITH "strict" "pattern" OPT ( "at" "level" natural ) | DELETE "strict" "pattern" @@ -1367,31 +1358,31 @@ syntax_extension_type: [ | DELETE "constr" (* covered by another prod *) ] -numnotoption: [ +numeral_modifier: [ | OPTINREF ] binder_tactic: [ -| REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5 -| WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" tactic_expr5 +| REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr5 +| WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr5 | MOVEALLBUT ltac_builtins ] -record_binder_body: [ -| REPLACE binders of_type_with_opt_coercion lconstr -| WITH binders of_type_with_opt_coercion -| REPLACE binders of_type_with_opt_coercion lconstr ":=" lconstr -| WITH binders of_type_with_opt_coercion ":=" lconstr +field_body: [ +| REPLACE binders of_type lconstr +| WITH binders of_type +| REPLACE binders of_type lconstr ":=" lconstr +| WITH binders of_type ":=" lconstr ] -simple_assum_coe: [ -| REPLACE LIST1 ident_decl of_type_with_opt_coercion lconstr -| WITH LIST1 ident_decl of_type_with_opt_coercion +assumpt: [ +| REPLACE LIST1 ident_decl of_type lconstr +| WITH LIST1 ident_decl of_type ] constructor_type: [ -| REPLACE binders [ of_type_with_opt_coercion lconstr | ] -| WITH binders OPT of_type_with_opt_coercion +| REPLACE binders [ of_type lconstr | ] +| WITH binders OPT of_type ] (* todo: is this really correct? Search for "Pvernac.register_proof_mode" *) @@ -1435,12 +1426,12 @@ legacy_attr: [ sentence: [ ] (* productions defined below *) -rec_definition: [ +fix_definition: [ | REPLACE ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations | WITH ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations ] -corec_definition: [ +cofix_definition: [ | REPLACE ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations | WITH ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations ] @@ -1457,7 +1448,7 @@ inductive_definition: [ ] (* note that constructor -> identref constructor_type *) -constructor_list_or_record_decl: [ +constructors_or_record: [ | DELETE "|" LIST1 constructor SEP "|" | REPLACE identref constructor_type "|" LIST1 constructor SEP "|" | WITH OPT "|" LIST1 constructor SEP "|" @@ -1468,8 +1459,8 @@ constructor_list_or_record_decl: [ ] record_binder: [ -| REPLACE name record_binder_body -| WITH name OPT record_binder_body +| REPLACE name field_body +| WITH name OPT field_body | DELETE name ] @@ -1636,7 +1627,7 @@ ltac2_rewriter: [ | OPT natural OPT [ "?" | "!" ] ltac2_constr_with_bindings ] -tac2expr0: [ +ltac2_expr0: [ | DELETE "(" ")" ] @@ -1813,9 +1804,9 @@ input_fun: [ ] let_clause: [ -| DELETE identref ":=" tactic_expr5 -| REPLACE "_" ":=" tactic_expr5 -| WITH name ":=" tactic_expr5 +| DELETE identref ":=" ltac_expr5 +| REPLACE "_" ":=" ltac_expr5 +| WITH name ":=" ltac_expr5 ] tactic_mode: [ @@ -1837,11 +1828,11 @@ tactic_mode: [ tactic_mode: [ | DELETENT ] -sexpr: [ +ltac2_scope: [ | REPLACE syn_node (* Ltac2 plugin *) | WITH name TAG Ltac2 -| REPLACE syn_node "(" LIST1 sexpr SEP "," ")" (* Ltac2 plugin *) -| WITH name "(" LIST1 sexpr SEP "," ")" TAG Ltac2 +| REPLACE syn_node "(" LIST1 ltac2_scope SEP "," ")" (* Ltac2 plugin *) +| WITH name "(" LIST1 ltac2_scope SEP "," ")" TAG Ltac2 ] syn_node: [ | DELETENT ] @@ -1851,7 +1842,7 @@ RENAME: [ ] toplevel_selector: [ -| selector_body +| selector | "all" | "!" (* par is accepted even though it's not in the .mlg *) @@ -1859,7 +1850,7 @@ toplevel_selector: [ ] toplevel_selector_temp: [ -| DELETE selector_body ":" +| DELETE selector ":" | DELETE "all" ":" | DELETE "!" ":" | toplevel_selector ":" @@ -1900,7 +1891,7 @@ query_command: [ ] (* re-add as a placeholder *) sentence: [ | OPT attributes command "." | OPT attributes OPT ( natural ":" ) query_command "." -| OPT attributes OPT ( toplevel_selector ":" ) tactic_expr5 [ "." | "..." ] +| OPT attributes OPT ( toplevel_selector ":" ) ltac_expr5 [ "." | "..." ] | control_command ] @@ -1924,18 +1915,18 @@ ltac_defined_tactics: [ | "split_Rabs" | "split_Rmult" | "tauto" -| "time_constr" tactic_expr5 +| "time_constr" ltac_expr5 | "zify" ] (* todo: need careful review; assume that "[" ... "]" are literals *) tactic_notation_tactics: [ -| "assert_fails" tactic_expr3 -| "assert_succeeds" tactic_expr3 +| "assert_fails" ltac_expr3 +| "assert_succeeds" ltac_expr3 | "field" OPT ( "[" LIST1 constr "]" ) | "field_simplify" OPT ( "[" LIST1 constr "]" ) LIST1 constr OPT ( "in" ident ) | "field_simplify_eq" OPT ( "[" LIST1 constr "]" ) OPT ( "in" ident ) -| "intuition" OPT tactic_expr5 +| "intuition" OPT ltac_expr5 | "nsatz" OPT ( "with" "radicalmax" ":=" constr "strategy" ":=" constr "parameters" ":=" constr "variables" ":=" constr ) | "psatz" constr OPT int_or_var | "ring" OPT ( "[" LIST1 constr "]" ) @@ -1943,8 +1934,8 @@ tactic_notation_tactics: [ ] (* defined in OCaml outside of mlgs *) -tactic_arg: [ -| "uconstr" ":" "(" operconstr200 ")" +tactic_value: [ +| "uconstr" ":" "(" term200 ")" | MOVEALLBUT simple_tactic ] @@ -1952,10 +1943,6 @@ nonterminal: [ ] value_tactic: [ ] -RENAME: [ -| tactic_arg tactic_value -] - syn_value: [ | IDENT; ":" "(" nonterminal ")" ] @@ -1974,8 +1961,8 @@ ltac2_match_key: [ ] ltac2_constructs: [ -| ltac2_match_key tac2expr6 "with" ltac2_match_list "end" -| ltac2_match_key OPT "reverse" "goal" "with" gmatch_list "end" +| ltac2_match_key ltac2_expr6 "with" ltac2_match_list "end" +| ltac2_match_key OPT "reverse" "goal" "with" goal_match_list "end" ] simple_tactic: [ @@ -1987,9 +1974,9 @@ simple_tactic: [ ] tacdef_body: [ -| REPLACE global LIST1 input_fun ltac_def_kind tactic_expr5 -| WITH global LIST0 input_fun ltac_def_kind tactic_expr5 -| DELETE global ltac_def_kind tactic_expr5 +| REPLACE global LIST1 input_fun ltac_def_kind ltac_expr5 +| WITH global LIST0 input_fun ltac_def_kind ltac_expr5 +| DELETE global ltac_def_kind ltac_expr5 ] tac2def_typ: [ @@ -2071,7 +2058,7 @@ atomic_tac2pat: [ | OPTINREF ] -tac2expr0: [ +ltac2_expr0: [ (* | DELETE "(" ")" (* covered by "()" prodn *) | REPLACE "{" [ | LIST1 tac2rec_fieldexpr OPT ";" ] "}" @@ -2084,13 +2071,13 @@ tac2expr0: [ use LIST1? *) SPLICE: [ -| tac2expr4 +| ltac2_expr4 ] -tac2expr3: [ -| REPLACE tac2expr2 "," LIST1 tac2expr2 SEP "," (* Ltac2 plugin *) -| WITH LIST1 tac2expr2 SEP "," TAG Ltac2 -| DELETE tac2expr2 (* Ltac2 plugin *) +ltac2_expr3: [ +| REPLACE ltac2_expr2 "," LIST1 ltac2_expr2 SEP "," (* Ltac2 plugin *) +| WITH LIST1 ltac2_expr2 SEP "," TAG Ltac2 +| DELETE ltac2_expr2 (* Ltac2 plugin *) ] tac2rec_fieldexprs: [ @@ -2171,7 +2158,7 @@ ltac2_entry: [ | WITH "Ltac2" tac2def_val | REPLACE tac2def_ext (* Ltac2 plugin *) | WITH "Ltac2" tac2def_ext -| "Ltac2" "Notation" [ string | lident ] ":=" tac2expr6 TAG Ltac2 (* variant *) +| "Ltac2" "Notation" [ string | lident ] ":=" ltac2_expr6 TAG Ltac2 (* variant *) | MOVEALLBUT command (* todo: MOVEALLBUT should ignore tag on "but" prodns *) ] @@ -2207,21 +2194,14 @@ SPLICE: [ | anti ] -tac2expr5: [ -| REPLACE "let" OPT "rec" LIST1 ltac2_let_clause SEP "with" "in" tac2expr6 (* Ltac2 plugin *) -| WITH "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" tac2expr6 TAG Ltac2 -| MOVETO simple_tactic "match" tac2expr5 "with" OPT ltac2_branches "end" (* Ltac2 plugin *) +ltac2_expr5: [ +| REPLACE "let" OPT "rec" LIST1 ltac2_let_clause SEP "with" "in" ltac2_expr6 (* Ltac2 plugin *) +| WITH "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" ltac2_expr6 TAG Ltac2 +| MOVETO simple_tactic "match" ltac2_expr5 "with" OPT ltac2_branches "end" (* Ltac2 plugin *) | DELETE simple_tactic ] -RENAME: [ -| Prim.string string -| Prim.integer integer -| Prim.qualid qualid -| Prim.natural natural -] - -gmatch_list: [ +goal_match_list: [ | EDIT ADD_OPT "|" LIST1 gmatch_rule SEP "|" (* Ltac2 plugin *) ] @@ -2290,6 +2270,10 @@ subprf: [ | "{" (* should be removed. See https://github.com/coq/coq/issues/12004 *) ] +ltac2_expr: [ +| DELETE _ltac2_expr +] + SPLICE: [ | clause | noedit_mode @@ -2309,10 +2293,10 @@ SPLICE: [ | ltac_selector | Constr.ident | attribute_list -| operconstr99 -| operconstr90 -| operconstr9 -| operconstr8 +| term99 +| term90 +| term9 +| term8 | pattern200 | pattern99 | pattern90 @@ -2363,7 +2347,7 @@ SPLICE: [ | check_module_types | constr_pattern | decl_sep -| function_rec_definition_loc (* loses funind annotation *) +| function_fix_definition (* loses funind annotation *) | glob | glob_constr_with_bindings | id_or_meta @@ -2381,7 +2365,6 @@ SPLICE: [ | decorated_vernac | ext_module_expr | ext_module_type -| pattern_ident | test | binder_constr | atomic_constr @@ -2449,7 +2432,6 @@ SPLICE: [ | intropatterns | instance_name | failkw -| selector | ne_in_or_out_modules | search_queries | locatable @@ -2472,7 +2454,6 @@ SPLICE: [ | refglobals (* Ltac2 *) | syntax_modifiers | array_elems -| ltac2_expr | G_LTAC2_input_fun | ltac2_simple_intropattern_closed | ltac2_with_bindings @@ -2489,81 +2470,33 @@ RENAME: [ | tactic3 ltac_expr3 (* todo: can't figure out how this gets mapped by coqpp *) | tactic1 ltac_expr1 (* todo: can't figure out how this gets mapped by coqpp *) | tactic0 ltac_expr0 (* todo: can't figure out how this gets mapped by coqpp *) -| ltac1_expr ltac_expr -| tactic_expr5 ltac_expr -| tactic_expr4 ltac_expr4 -| tactic_expr3 ltac_expr3 -| tactic_expr2 ltac_expr2 -| tactic_expr1 ltac_expr1 -| tactic_expr0 ltac_expr0 +| ltac_expr5 ltac_expr (* | nonsimple_intropattern intropattern (* ltac2 *) *) -| operconstr200 term (* historical name *) -| operconstr100 term100 -| operconstr10 term10 -| operconstr1 term1 -| operconstr0 term0 +| term200 term | pattern100 pattern -| match_constr term_match (*| impl_ident_tail impl_ident*) | ssexpr50 section_var_expr50 | ssexpr0 section_var_expr0 | section_subset_expr section_var_expr | fun_scheme_arg func_scheme_def -| tactic_then_gen for_each_goal -| ltac2_tactic_then_gen ltac2_for_each_goal -| selector_body selector -| match_hyps match_hyp - | BULLET bullet -| fix_decl fix_body -| cofix_decl cofix_body -(* todo: it's confusing that Constr.constr and constr mean different things *) -| constr one_term -| appl_arg arg -| rec_definition fix_definition -| corec_definition cofix_definition -| univ_instance univ_annot -| simple_assum_coe assumpt -| of_type_with_opt_coercion of_type -| attribute_value attr_value -| constructor_list_or_record_decl constructors_or_record -| record_binder_body field_body -| class_rawexpr class -| smart_global reference +| constr one_term (* many, many, many *) +| class_rawexpr class (* OCaml reserved word *) +| smart_global reference (* many, many *) (* | searchabout_query search_item *) -| option_table setting_name -| argument_spec_block arg_specs -| more_implicits_block implicits_alt -| arguments_modifier args_modifier -| constr_as_binder_kind binder_interp -| syntax_extension_type explicit_subentry -| numnotoption numeral_modifier -| tactic_arg_compat tactic_arg -| lconstr_pattern cpattern -| Pltac.tactic ltac_expr -| sexpr ltac2_scope -| tac2type5 ltac2_type -| tac2type2 ltac2_type2 -| tac2type1 ltac2_type1 -| tac2type0 ltac2_type0 -| typ_param ltac2_typevar -| tac2expr6 ltac2_expr -| tac2expr5 ltac2_expr5 -| tac2expr3 ltac2_expr3 -| tac2expr2 ltac2_expr2 -| tac2expr1 ltac2_expr1 -| tac2expr0 ltac2_expr0 -| gmatch_list goal_match_list +| Pltac.tactic ltac_expr (* many uses in EXTENDs *) +| ltac2_type5 ltac2_type +| ltac2_expr6 ltac2_expr | starredidentref starred_ident_ref ] simple_tactic: [ -(* due to renaming of tactic_arg; Use LIST1 for function application *) +(* due to renaming of tactic_value; Use LIST1 for function application *) | qualid LIST1 tactic_arg ] @@ -2585,7 +2518,7 @@ SPLICE: [ | ltac_defined_tactics | tactic_notation_tactics ] -(* todo: ssrreflect*.rst ref to fix_body is incorrect *) +(* todo: ssrreflect*.rst ref to fix_decl is incorrect *) REACHABLE: [ | command @@ -2624,17 +2557,7 @@ NOTINRSTS: [ | q_constr_matching | q_goal_matching -(* todo: figure these out -(*Warning: editedGrammar: Undefined symbol 'ltac1_expr' *) -| dangling_pattern_extension_rule -| vernac_aux -| subprf -| tactic_mode -| tac2expr_in_env (* no refs *) -| tac2mode (* no refs *) -| ltac_use_default (* from tac2mode *) -| tacticals -*) + ] REACHABLE: [ diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index d3148b5e3a..c764cb6f37 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -17,7 +17,7 @@ constr_pattern: [ | constr ] -lconstr_pattern: [ +cpattern: [ | lconstr ] @@ -58,67 +58,67 @@ universe: [ ] lconstr: [ -| operconstr200 +| term200 ] constr: [ -| operconstr8 -| "@" global univ_instance +| term8 +| "@" global univ_annot ] -operconstr200: [ +term200: [ | binder_constr -| operconstr100 +| term100 ] -operconstr100: [ -| operconstr99 "<:" operconstr200 -| operconstr99 "<<:" operconstr200 -| operconstr99 ":" operconstr200 -| operconstr99 ":>" -| operconstr99 +term100: [ +| term99 "<:" term200 +| term99 "<<:" term200 +| term99 ":" term200 +| term99 ":>" +| term99 ] -operconstr99: [ -| operconstr90 +term99: [ +| term90 ] -operconstr90: [ -| operconstr10 +term90: [ +| term10 ] -operconstr10: [ -| operconstr9 LIST1 appl_arg -| "@" global univ_instance LIST0 operconstr9 +term10: [ +| term9 LIST1 arg +| "@" global univ_annot LIST0 term9 | "@" pattern_ident LIST1 identref -| operconstr9 +| term9 ] -operconstr9: [ -| ".." operconstr0 ".." -| operconstr8 +term9: [ +| ".." term0 ".." +| term8 ] -operconstr8: [ -| operconstr1 +term8: [ +| term1 ] -operconstr1: [ -| operconstr0 ".(" global LIST0 appl_arg ")" -| operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")" -| operconstr0 "%" IDENT -| operconstr0 +term1: [ +| term0 ".(" global LIST0 arg ")" +| term0 ".(" "@" global LIST0 ( term9 ) ")" +| term0 "%" IDENT +| term0 ] -operconstr0: [ +term0: [ | atomic_constr -| match_constr -| "(" operconstr200 ")" +| term_match +| "(" term200 ")" | "{|" record_declaration bar_cbrace | "{" binder_constr "}" -| "`{" operconstr200 "}" -| test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_instance -| "`(" operconstr200 ")" +| "`{" term200 "}" +| test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_annot +| "`(" term200 ")" ] array_elems: [ @@ -140,27 +140,27 @@ field_def: [ ] binder_constr: [ -| "forall" open_binders "," operconstr200 -| "fun" open_binders "=>" operconstr200 -| "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200 -| "let" "fix" fix_decl "in" operconstr200 -| "let" "cofix" cofix_decl "in" operconstr200 -| "let" [ "(" LIST0 name SEP "," ")" | "()" ] return_type ":=" operconstr200 "in" operconstr200 -| "let" "'" pattern200 ":=" operconstr200 "in" operconstr200 -| "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200 -| "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200 -| "if" operconstr200 return_type "then" operconstr200 "else" operconstr200 +| "forall" open_binders "," term200 +| "fun" open_binders "=>" term200 +| "let" name binders let_type_cstr ":=" term200 "in" term200 +| "let" "fix" fix_decl "in" term200 +| "let" "cofix" cofix_body "in" term200 +| "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200 +| "let" "'" pattern200 ":=" term200 "in" term200 +| "let" "'" pattern200 ":=" term200 case_type "in" term200 +| "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200 +| "if" term200 as_return_type "then" term200 "else" term200 | "fix" fix_decls | "cofix" cofix_decls ] -appl_arg: [ +arg: [ | test_lpar_id_coloneq "(" identref ":=" lconstr ")" -| operconstr9 +| term9 ] atomic_constr: [ -| global univ_instance +| global univ_annot | sort | NUMBER | string @@ -179,7 +179,7 @@ evar_instance: [ | ] -univ_instance: [ +univ_annot: [ | "@{" LIST0 universe_level "}" | ] @@ -198,31 +198,31 @@ fix_decls: [ ] cofix_decls: [ -| cofix_decl -| cofix_decl "with" LIST1 cofix_decl SEP "with" "for" identref +| cofix_body +| cofix_body "with" LIST1 cofix_body SEP "with" "for" identref ] fix_decl: [ -| identref binders_fixannot type_cstr ":=" operconstr200 +| identref binders_fixannot type_cstr ":=" term200 ] -cofix_decl: [ -| identref binders type_cstr ":=" operconstr200 +cofix_body: [ +| identref binders type_cstr ":=" term200 ] -match_constr: [ +term_match: [ | "match" LIST1 case_item SEP "," OPT case_type "with" branches "end" ] case_item: [ -| operconstr100 OPT [ "as" name ] OPT [ "in" pattern200 ] +| term100 OPT [ "as" name ] OPT [ "in" pattern200 ] ] case_type: [ -| "return" operconstr100 +| "return" term100 ] -return_type: [ +as_return_type: [ | OPT [ OPT [ "as" name ] case_type ] ] @@ -253,7 +253,7 @@ pattern200: [ ] pattern100: [ -| pattern99 ":" operconstr200 +| pattern99 ":" term200 | pattern99 ] @@ -335,10 +335,10 @@ closed_binder: [ ] typeclass_constraint: [ -| "!" operconstr200 -| "{" name "}" ":" [ "!" | ] operconstr200 -| test_name_colon name ":" [ "!" | ] operconstr200 -| operconstr200 +| "!" term200 +| "{" name "}" ":" [ "!" | ] term200 +| test_name_colon name ":" [ "!" | ] term200 +| term200 ] type_cstr: [ @@ -506,7 +506,7 @@ command: [ | "Remove" "Hints" LIST1 global opt_hintbases | "Hint" hint opt_hintbases | "Comments" LIST0 comment -| "Declare" "Instance" ident_decl binders ":" operconstr200 hint_info +| "Declare" "Instance" ident_decl binders ":" term200 hint_info | "Declare" "Scope" IDENT | "Pwd" | "Cd" @@ -525,13 +525,13 @@ command: [ | "Print" "Namespace" dirpath | "Inspect" natural | "Add" "ML" "Path" ne_string -| "Set" option_table option_setting -| "Unset" option_table -| "Print" "Table" option_table +| "Set" setting_name option_setting +| "Unset" setting_name +| "Print" "Table" setting_name | "Add" IDENT IDENT LIST1 table_value | "Add" IDENT LIST1 table_value -| "Test" option_table "for" LIST1 table_value -| "Test" option_table +| "Test" setting_name "for" LIST1 table_value +| "Test" setting_name | "Remove" IDENT IDENT LIST1 table_value | "Remove" IDENT LIST1 table_value | "Write" "State" IDENT @@ -569,7 +569,7 @@ command: [ | "Show" "Extraction" (* extraction plugin *) | "Set" "Firstorder" "Solver" tactic | "Print" "Firstorder" "Solver" -| "Function" LIST1 function_rec_definition_loc SEP "with" (* funind plugin *) +| "Function" LIST1 function_fix_definition SEP "with" (* funind plugin *) | "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with" (* funind plugin *) | "Functional" "Case" fun_scheme_arg (* funind plugin *) | "Generate" "graph" "for" reference (* funind plugin *) @@ -686,11 +686,11 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" constr OPT field_mods (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Number" "Notation" reference reference reference ":" ident numnotoption -| "Numeral" "Notation" reference reference reference ":" ident numnotoption +| "Number" "Notation" reference reference reference ":" ident numeral_modifier +| "Numeral" "Notation" reference reference reference ":" ident numeral_modifier | "String" "Notation" reference reference reference ":" ident | "Ltac2" ltac2_entry (* Ltac2 plugin *) -| "Ltac2" "Eval" ltac2_expr (* Ltac2 plugin *) +| "Ltac2" "Eval" ltac2_expr6 (* Ltac2 plugin *) | "Print" "Ltac2" reference (* Ltac2 plugin *) ] @@ -745,10 +745,10 @@ attribute_list: [ ] attribute: [ -| ident attribute_value +| ident attr_value ] -attribute_value: [ +attr_value: [ | "=" string | "(" attribute_list ")" | @@ -795,10 +795,10 @@ gallina: [ | def_token ident_decl def_body | "Let" ident_decl def_body | finite_token LIST1 inductive_definition SEP "with" -| "Fixpoint" LIST1 rec_definition SEP "with" -| "Let" "Fixpoint" LIST1 rec_definition SEP "with" -| "CoFixpoint" LIST1 corec_definition SEP "with" -| "Let" "CoFixpoint" LIST1 corec_definition SEP "with" +| "Fixpoint" LIST1 fix_definition SEP "with" +| "Let" "Fixpoint" LIST1 fix_definition SEP "with" +| "CoFixpoint" LIST1 cofix_definition SEP "with" +| "Let" "CoFixpoint" LIST1 cofix_definition SEP "with" | "Scheme" LIST1 scheme SEP "with" | "Combined" "Scheme" identref "from" LIST1 identref SEP "," | "Register" global "as" qualid @@ -897,7 +897,7 @@ decl_notations: [ ] opt_constructors_or_fields: [ -| ":=" constructor_list_or_record_decl +| ":=" constructors_or_record | ] @@ -905,7 +905,7 @@ inductive_definition: [ | opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations ] -constructor_list_or_record_decl: [ +constructors_or_record: [ | "|" LIST1 constructor SEP "|" | identref constructor_type "|" LIST1 constructor SEP "|" | identref constructor_type @@ -919,11 +919,11 @@ opt_coercion: [ | ] -rec_definition: [ +fix_definition: [ | ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations ] -corec_definition: [ +cofix_definition: [ | ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations ] @@ -950,39 +950,39 @@ record_fields: [ | ] -record_binder_body: [ -| binders of_type_with_opt_coercion lconstr -| binders of_type_with_opt_coercion lconstr ":=" lconstr +field_body: [ +| binders of_type lconstr +| binders of_type lconstr ":=" lconstr | binders ":=" lconstr ] record_binder: [ | name -| name record_binder_body +| name field_body ] assum_list: [ | LIST1 assum_coe -| simple_assum_coe +| assumpt ] assum_coe: [ -| "(" simple_assum_coe ")" +| "(" assumpt ")" ] -simple_assum_coe: [ -| LIST1 ident_decl of_type_with_opt_coercion lconstr +assumpt: [ +| LIST1 ident_decl of_type lconstr ] constructor_type: [ -| binders [ of_type_with_opt_coercion lconstr | ] +| binders [ of_type lconstr | ] ] constructor: [ | identref constructor_type ] -of_type_with_opt_coercion: [ +of_type: [ | ":>" | ":" ">" | ":" @@ -1011,16 +1011,16 @@ gallina_ext: [ | "Coercion" global ":" class_rawexpr ">->" class_rawexpr | "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr | "Context" LIST1 binder -| "Instance" instance_name ":" operconstr200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ] +| "Instance" instance_name ":" term200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ] | "Existing" "Instance" global hint_info | "Existing" "Instances" LIST1 global OPT [ "|" natural ] | "Existing" "Class" global -| "Arguments" smart_global LIST0 argument_spec_block OPT [ "," LIST1 [ LIST0 more_implicits_block ] SEP "," ] OPT [ ":" LIST1 arguments_modifier SEP "," ] +| "Arguments" smart_global LIST0 arg_specs OPT [ "," LIST1 [ LIST0 implicits_alt ] SEP "," ] OPT [ ":" LIST1 args_modifier SEP "," ] | "Implicit" "Type" reserv_list | "Implicit" "Types" reserv_list | "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 identref ] -| "Export" "Set" option_table option_setting -| "Export" "Unset" option_table +| "Export" "Set" setting_name option_setting +| "Export" "Unset" setting_name ] filtered_import: [ @@ -1142,7 +1142,7 @@ ssexpr0: [ | "(" ssexpr35 ")" "*" ] -arguments_modifier: [ +args_modifier: [ | "simpl" "nomatch" | "simpl" "never" | "default" "implicits" @@ -1164,7 +1164,7 @@ argument_spec: [ | OPT "!" name OPT scope_delimiter ] -argument_spec_block: [ +arg_specs: [ | argument_spec | "/" | "&" @@ -1173,7 +1173,7 @@ argument_spec_block: [ | "{" LIST1 argument_spec "}" OPT scope_delimiter ] -more_implicits_block: [ +implicits_alt: [ | name | "[" LIST1 name "]" | "{" LIST1 name "}" @@ -1282,7 +1282,7 @@ table_value: [ | STRING ] -option_table: [ +setting_name: [ | LIST1 IDENT ] @@ -1391,9 +1391,9 @@ syntax_modifier: [ | "only" "parsing" | "format" STRING OPT STRING | IDENT; "," LIST1 IDENT SEP "," "at" level -| IDENT; "at" level OPT constr_as_binder_kind -| IDENT constr_as_binder_kind -| IDENT syntax_extension_type +| IDENT; "at" level OPT binder_interp +| IDENT binder_interp +| IDENT explicit_subentry ] syntax_modifiers: [ @@ -1401,19 +1401,19 @@ syntax_modifiers: [ | ] -syntax_extension_type: [ +explicit_subentry: [ | "ident" | "global" | "bigint" | "binder" | "constr" -| "constr" at_level_opt OPT constr_as_binder_kind +| "constr" at_level_opt OPT binder_interp | "pattern" | "pattern" "at" "level" natural | "strict" "pattern" | "strict" "pattern" "at" "level" natural | "closed" "binder" -| "custom" IDENT at_level_opt OPT constr_as_binder_kind +| "custom" IDENT at_level_opt OPT binder_interp ] at_level_opt: [ @@ -1421,7 +1421,7 @@ at_level_opt: [ | ] -constr_as_binder_kind: [ +binder_interp: [ | "as" "ident" | "as" "pattern" | "as" "strict" "pattern" @@ -1789,8 +1789,8 @@ auto_using': [ | (* funind plugin *) ] -function_rec_definition_loc: [ -| Vernac.rec_definition (* funind plugin *) +function_fix_definition: [ +| Vernac.fix_definition (* funind plugin *) ] fun_scheme_arg: [ @@ -1923,16 +1923,16 @@ eauto_search_strategy: [ ] tactic_then_last: [ -| "|" LIST0 ( OPT tactic_expr5 ) SEP "|" +| "|" LIST0 ( OPT ltac_expr5 ) SEP "|" | ] -tactic_then_gen: [ -| tactic_expr5 "|" tactic_then_gen -| tactic_expr5 ".." tactic_then_last +for_each_goal: [ +| ltac_expr5 "|" for_each_goal +| ltac_expr5 ".." tactic_then_last | ".." tactic_then_last -| tactic_expr5 -| "|" tactic_then_gen +| ltac_expr5 +| "|" for_each_goal | ] @@ -1940,60 +1940,60 @@ tactic_then_locality: [ | "[" OPT ">" ] -tactic_expr5: [ +ltac_expr5: [ | binder_tactic -| tactic_expr4 -] - -tactic_expr4: [ -| tactic_expr3 ";" binder_tactic -| tactic_expr3 ";" tactic_expr3 -| tactic_expr3 ";" tactic_then_locality tactic_then_gen "]" -| tactic_expr3 -] - -tactic_expr3: [ -| "try" tactic_expr3 -| "do" int_or_var tactic_expr3 -| "timeout" int_or_var tactic_expr3 -| "time" OPT string tactic_expr3 -| "repeat" tactic_expr3 -| "progress" tactic_expr3 -| "once" tactic_expr3 -| "exactly_once" tactic_expr3 -| "infoH" tactic_expr3 -| "abstract" tactic_expr2 -| "abstract" tactic_expr2 "using" ident -| selector tactic_expr3 -| tactic_expr2 -] - -tactic_expr2: [ -| tactic_expr1 "+" binder_tactic -| tactic_expr1 "+" tactic_expr2 -| "tryif" tactic_expr5 "then" tactic_expr5 "else" tactic_expr2 -| tactic_expr1 "||" binder_tactic -| tactic_expr1 "||" tactic_expr2 -| tactic_expr1 -] - -tactic_expr1: [ +| ltac_expr4 +] + +ltac_expr4: [ +| ltac_expr3 ";" binder_tactic +| ltac_expr3 ";" ltac_expr3 +| ltac_expr3 ";" tactic_then_locality for_each_goal "]" +| ltac_expr3 +] + +ltac_expr3: [ +| "try" ltac_expr3 +| "do" int_or_var ltac_expr3 +| "timeout" int_or_var ltac_expr3 +| "time" OPT string ltac_expr3 +| "repeat" ltac_expr3 +| "progress" ltac_expr3 +| "once" ltac_expr3 +| "exactly_once" ltac_expr3 +| "infoH" ltac_expr3 +| "abstract" ltac_expr2 +| "abstract" ltac_expr2 "using" ident +| "only" selector ":" ltac_expr3 +| ltac_expr2 +] + +ltac_expr2: [ +| ltac_expr1 "+" binder_tactic +| ltac_expr1 "+" ltac_expr2 +| "tryif" ltac_expr5 "then" ltac_expr5 "else" ltac_expr2 +| ltac_expr1 "||" binder_tactic +| ltac_expr1 "||" ltac_expr2 +| ltac_expr1 +] + +ltac_expr1: [ | match_key "goal" "with" match_context_list "end" | match_key "reverse" "goal" "with" match_context_list "end" -| match_key tactic_expr5 "with" match_list "end" -| "first" "[" LIST0 tactic_expr5 SEP "|" "]" -| "solve" "[" LIST0 tactic_expr5 SEP "|" "]" +| match_key ltac_expr5 "with" match_list "end" +| "first" "[" LIST0 ltac_expr5 SEP "|" "]" +| "solve" "[" LIST0 ltac_expr5 SEP "|" "]" | "idtac" LIST0 message_token | failkw [ int_or_var | ] LIST0 message_token | simple_tactic -| tactic_arg -| reference LIST0 tactic_arg_compat -| tactic_expr0 +| tactic_value +| reference LIST0 tactic_arg +| ltac_expr0 ] -tactic_expr0: [ -| "(" tactic_expr5 ")" -| "[" ">" tactic_then_gen "]" +ltac_expr0: [ +| "(" ltac_expr5 ")" +| "[" ">" for_each_goal "]" | tactic_atom ] @@ -2003,17 +2003,17 @@ failkw: [ ] binder_tactic: [ -| "fun" LIST1 input_fun "=>" tactic_expr5 -| "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5 +| "fun" LIST1 input_fun "=>" ltac_expr5 +| "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr5 ] -tactic_arg_compat: [ -| tactic_arg +tactic_arg: [ +| tactic_value | Constr.constr | "()" ] -tactic_arg: [ +tactic_value: [ | constr_eval | "fresh" LIST0 fresh_id | "type_term" uconstr @@ -2054,26 +2054,26 @@ input_fun: [ ] let_clause: [ -| identref ":=" tactic_expr5 -| "_" ":=" tactic_expr5 -| identref LIST1 input_fun ":=" tactic_expr5 +| identref ":=" ltac_expr5 +| "_" ":=" ltac_expr5 +| identref LIST1 input_fun ":=" ltac_expr5 ] match_pattern: [ -| "context" OPT Constr.ident "[" Constr.lconstr_pattern "]" -| Constr.lconstr_pattern +| "context" OPT Constr.ident "[" Constr.cpattern "]" +| Constr.cpattern ] -match_hyps: [ +match_hyp: [ | name ":" match_pattern | name ":=" "[" match_pattern "]" ":" match_pattern | name ":=" match_pattern ] match_context_rule: [ -| LIST0 match_hyps SEP "," "|-" match_pattern "=>" tactic_expr5 -| "[" LIST0 match_hyps SEP "," "|-" match_pattern "]" "=>" tactic_expr5 -| "_" "=>" tactic_expr5 +| LIST0 match_hyp SEP "," "|-" match_pattern "=>" ltac_expr5 +| "[" LIST0 match_hyp SEP "," "|-" match_pattern "]" "=>" ltac_expr5 +| "_" "=>" ltac_expr5 ] match_context_list: [ @@ -2082,8 +2082,8 @@ match_context_list: [ ] match_rule: [ -| match_pattern "=>" tactic_expr5 -| "_" "=>" tactic_expr5 +| match_pattern "=>" ltac_expr5 +| "_" "=>" ltac_expr5 ] match_list: [ @@ -2103,12 +2103,12 @@ ltac_def_kind: [ ] tacdef_body: [ -| Constr.global LIST1 input_fun ltac_def_kind tactic_expr5 -| Constr.global ltac_def_kind tactic_expr5 +| Constr.global LIST1 input_fun ltac_def_kind ltac_expr5 +| Constr.global ltac_def_kind ltac_expr5 ] tactic: [ -| tactic_expr5 +| ltac_expr5 ] range_selector: [ @@ -2121,17 +2121,13 @@ range_selector_or_nth: [ | natural OPT [ "," LIST1 range_selector SEP "," ] ] -selector_body: [ +selector: [ | range_selector_or_nth | test_bracket_ident "[" ident "]" ] -selector: [ -| "only" selector_body ":" -] - toplevel_selector: [ -| selector_body ":" +| selector ":" | "!" ":" | "all" ":" ] @@ -2147,8 +2143,8 @@ G_LTAC_hint: [ | "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic ] -G_LTAC_operconstr0: [ -| "ltac" ":" "(" Pltac.tactic_expr ")" +G_LTAC_term0: [ +| "ltac" ":" "(" Pltac.ltac_expr ")" ] ltac_selector: [ @@ -2327,7 +2323,7 @@ intropattern: [ ] simple_intropattern: [ -| simple_intropattern_closed LIST0 [ "%" operconstr0 ] +| simple_intropattern_closed LIST0 [ "%" term0 ] ] simple_intropattern_closed: [ @@ -2356,7 +2352,7 @@ with_bindings: [ | ] -red_flags: [ +red_flag: [ | "beta" | "iota" | "match" @@ -2373,7 +2369,7 @@ delta_flag: [ ] strategy_flag: [ -| LIST1 red_flags +| LIST1 red_flag | delta_flag ] @@ -2500,7 +2496,7 @@ as_name: [ ] by_tactic: [ -| "by" tactic_expr3 +| "by" ltac_expr3 | ] @@ -2553,7 +2549,7 @@ field_mods: [ | "(" LIST1 field_mod SEP "," ")" (* ring plugin *) ] -numnotoption: [ +numeral_modifier: [ | | "(" "warning" "after" bignat ")" | "(" "abstract" "after" bignat ")" @@ -2576,50 +2572,50 @@ tac2pat0: [ atomic_tac2pat: [ | (* Ltac2 plugin *) -| tac2pat1 ":" tac2type5 (* Ltac2 plugin *) +| tac2pat1 ":" ltac2_type5 (* Ltac2 plugin *) | tac2pat1 "," LIST0 tac2pat1 SEP "," (* Ltac2 plugin *) | tac2pat1 (* Ltac2 plugin *) ] -tac2expr6: [ -| tac2expr5 ";" tac2expr6 (* Ltac2 plugin *) -| tac2expr5 (* Ltac2 plugin *) +ltac2_expr6: [ +| ltac2_expr5 ";" ltac2_expr6 (* Ltac2 plugin *) +| ltac2_expr5 (* Ltac2 plugin *) ] -tac2expr5: [ -| "fun" LIST1 G_LTAC2_input_fun "=>" tac2expr6 (* Ltac2 plugin *) -| "let" rec_flag LIST1 G_LTAC2_let_clause SEP "with" "in" tac2expr6 (* Ltac2 plugin *) -| "match" tac2expr5 "with" G_LTAC2_branches "end" (* Ltac2 plugin *) -| tac2expr4 (* Ltac2 plugin *) +ltac2_expr5: [ +| "fun" LIST1 G_LTAC2_input_fun "=>" ltac2_expr6 (* Ltac2 plugin *) +| "let" rec_flag LIST1 G_LTAC2_let_clause SEP "with" "in" ltac2_expr6 (* Ltac2 plugin *) +| "match" ltac2_expr5 "with" G_LTAC2_branches "end" (* Ltac2 plugin *) +| ltac2_expr4 (* Ltac2 plugin *) ] -tac2expr4: [ -| tac2expr3 (* Ltac2 plugin *) +ltac2_expr4: [ +| ltac2_expr3 (* Ltac2 plugin *) ] -tac2expr3: [ -| tac2expr2 "," LIST1 tac2expr2 SEP "," (* Ltac2 plugin *) -| tac2expr2 (* Ltac2 plugin *) +ltac2_expr3: [ +| ltac2_expr2 "," LIST1 ltac2_expr2 SEP "," (* Ltac2 plugin *) +| ltac2_expr2 (* Ltac2 plugin *) ] -tac2expr2: [ -| tac2expr1 "::" tac2expr2 (* Ltac2 plugin *) -| tac2expr1 (* Ltac2 plugin *) +ltac2_expr2: [ +| ltac2_expr1 "::" ltac2_expr2 (* Ltac2 plugin *) +| ltac2_expr1 (* Ltac2 plugin *) ] -tac2expr1: [ -| tac2expr0 LIST1 tac2expr0 (* Ltac2 plugin *) -| tac2expr0 ".(" Prim.qualid ")" (* Ltac2 plugin *) -| tac2expr0 ".(" Prim.qualid ")" ":=" tac2expr5 (* Ltac2 plugin *) -| tac2expr0 (* Ltac2 plugin *) +ltac2_expr1: [ +| ltac2_expr0 LIST1 ltac2_expr0 (* Ltac2 plugin *) +| ltac2_expr0 ".(" Prim.qualid ")" (* Ltac2 plugin *) +| ltac2_expr0 ".(" Prim.qualid ")" ":=" ltac2_expr5 (* Ltac2 plugin *) +| ltac2_expr0 (* Ltac2 plugin *) ] -tac2expr0: [ -| "(" tac2expr6 ")" (* Ltac2 plugin *) -| "(" tac2expr6 ":" tac2type5 ")" (* Ltac2 plugin *) +ltac2_expr0: [ +| "(" ltac2_expr6 ")" (* Ltac2 plugin *) +| "(" ltac2_expr6 ":" ltac2_type5 ")" (* Ltac2 plugin *) | "()" (* Ltac2 plugin *) | "(" ")" (* Ltac2 plugin *) -| "[" LIST0 tac2expr5 SEP ";" "]" (* Ltac2 plugin *) +| "[" LIST0 ltac2_expr5 SEP ";" "]" (* Ltac2 plugin *) | "{" tac2rec_fieldexprs "}" (* Ltac2 plugin *) | G_LTAC2_tactic_atom (* Ltac2 plugin *) ] @@ -2631,7 +2627,7 @@ G_LTAC2_branches: [ ] branch: [ -| tac2pat1 "=>" tac2expr6 (* Ltac2 plugin *) +| tac2pat1 "=>" ltac2_expr6 (* Ltac2 plugin *) ] rec_flag: [ @@ -2644,7 +2640,7 @@ mut_flag: [ | (* Ltac2 plugin *) ] -typ_param: [ +ltac2_typevar: [ | "'" Prim.ident (* Ltac2 plugin *) ] @@ -2658,48 +2654,48 @@ G_LTAC2_tactic_atom: [ | "constr" ":" "(" Constr.lconstr ")" (* Ltac2 plugin *) | "open_constr" ":" "(" Constr.lconstr ")" (* Ltac2 plugin *) | "ident" ":" "(" lident ")" (* Ltac2 plugin *) -| "pattern" ":" "(" Constr.lconstr_pattern ")" (* Ltac2 plugin *) +| "pattern" ":" "(" Constr.cpattern ")" (* Ltac2 plugin *) | "reference" ":" "(" globref ")" (* Ltac2 plugin *) | "ltac1" ":" "(" ltac1_expr_in_env ")" (* Ltac2 plugin *) | "ltac1val" ":" "(" ltac1_expr_in_env ")" (* Ltac2 plugin *) ] ltac1_expr_in_env: [ -| test_ltac1_env LIST0 locident "|-" ltac1_expr (* Ltac2 plugin *) -| ltac1_expr (* Ltac2 plugin *) +| test_ltac1_env LIST0 locident "|-" ltac_expr5 (* Ltac2 plugin *) +| ltac_expr5 (* Ltac2 plugin *) ] tac2expr_in_env: [ -| test_ltac1_env LIST0 locident "|-" tac2expr6 (* Ltac2 plugin *) -| tac2expr6 (* Ltac2 plugin *) +| test_ltac1_env LIST0 locident "|-" ltac2_expr6 (* Ltac2 plugin *) +| ltac2_expr6 (* Ltac2 plugin *) ] G_LTAC2_let_clause: [ -| let_binder ":=" tac2expr6 (* Ltac2 plugin *) +| let_binder ":=" ltac2_expr6 (* Ltac2 plugin *) ] let_binder: [ | LIST1 G_LTAC2_input_fun (* Ltac2 plugin *) ] -tac2type5: [ -| tac2type2 "->" tac2type5 (* Ltac2 plugin *) -| tac2type2 (* Ltac2 plugin *) +ltac2_type5: [ +| ltac2_type2 "->" ltac2_type5 (* Ltac2 plugin *) +| ltac2_type2 (* Ltac2 plugin *) ] -tac2type2: [ -| tac2type1 "*" LIST1 tac2type1 SEP "*" (* Ltac2 plugin *) -| tac2type1 (* Ltac2 plugin *) +ltac2_type2: [ +| ltac2_type1 "*" LIST1 ltac2_type1 SEP "*" (* Ltac2 plugin *) +| ltac2_type1 (* Ltac2 plugin *) ] -tac2type1: [ -| tac2type0 Prim.qualid (* Ltac2 plugin *) -| tac2type0 (* Ltac2 plugin *) +ltac2_type1: [ +| ltac2_type0 Prim.qualid (* Ltac2 plugin *) +| ltac2_type0 (* Ltac2 plugin *) ] -tac2type0: [ -| "(" LIST1 tac2type5 SEP "," ")" OPT Prim.qualid (* Ltac2 plugin *) -| typ_param (* Ltac2 plugin *) +ltac2_type0: [ +| "(" LIST1 ltac2_type5 SEP "," ")" OPT Prim.qualid (* Ltac2 plugin *) +| ltac2_typevar (* Ltac2 plugin *) | "_" (* Ltac2 plugin *) | Prim.qualid (* Ltac2 plugin *) ] @@ -2718,7 +2714,7 @@ G_LTAC2_input_fun: [ ] tac2def_body: [ -| G_LTAC2_binder LIST0 G_LTAC2_input_fun ":=" tac2expr6 (* Ltac2 plugin *) +| G_LTAC2_binder LIST0 G_LTAC2_input_fun ":=" ltac2_expr6 (* Ltac2 plugin *) ] tac2def_val: [ @@ -2726,11 +2722,11 @@ tac2def_val: [ ] tac2def_mut: [ -| "Set" Prim.qualid OPT [ "as" locident ] ":=" tac2expr6 (* Ltac2 plugin *) +| "Set" Prim.qualid OPT [ "as" locident ] ":=" ltac2_expr6 (* Ltac2 plugin *) ] tac2typ_knd: [ -| tac2type5 (* Ltac2 plugin *) +| ltac2_type5 (* Ltac2 plugin *) | "[" ".." "]" (* Ltac2 plugin *) | "[" tac2alg_constructors "]" (* Ltac2 plugin *) | "{" tac2rec_fields "}" (* Ltac2 plugin *) @@ -2743,7 +2739,7 @@ tac2alg_constructors: [ tac2alg_constructor: [ | Prim.ident (* Ltac2 plugin *) -| Prim.ident "(" LIST0 tac2type5 SEP "," ")" (* Ltac2 plugin *) +| Prim.ident "(" LIST0 ltac2_type5 SEP "," ")" (* Ltac2 plugin *) ] tac2rec_fields: [ @@ -2754,7 +2750,7 @@ tac2rec_fields: [ ] tac2rec_field: [ -| mut_flag Prim.ident ":" tac2type5 (* Ltac2 plugin *) +| mut_flag Prim.ident ":" ltac2_type5 (* Ltac2 plugin *) ] tac2rec_fieldexprs: [ @@ -2765,13 +2761,13 @@ tac2rec_fieldexprs: [ ] tac2rec_fieldexpr: [ -| Prim.qualid ":=" tac2expr1 (* Ltac2 plugin *) +| Prim.qualid ":=" ltac2_expr1 (* Ltac2 plugin *) ] tac2typ_prm: [ | (* Ltac2 plugin *) -| typ_param (* Ltac2 plugin *) -| "(" LIST1 typ_param SEP "," ")" (* Ltac2 plugin *) +| ltac2_typevar (* Ltac2 plugin *) +| "(" LIST1 ltac2_typevar SEP "," ")" (* Ltac2 plugin *) ] tac2typ_def: [ @@ -2789,7 +2785,7 @@ tac2def_typ: [ ] tac2def_ext: [ -| "@" "external" locident ":" tac2type5 ":=" Prim.string Prim.string (* Ltac2 plugin *) +| "@" "external" locident ":" ltac2_type5 ":=" Prim.string Prim.string (* Ltac2 plugin *) ] syn_node: [ @@ -2797,11 +2793,11 @@ syn_node: [ | Prim.ident (* Ltac2 plugin *) ] -sexpr: [ +ltac2_scope: [ | Prim.string (* Ltac2 plugin *) | Prim.integer (* Ltac2 plugin *) | syn_node (* Ltac2 plugin *) -| syn_node "(" LIST1 sexpr SEP "," ")" (* Ltac2 plugin *) +| syn_node "(" LIST1 ltac2_scope SEP "," ")" (* Ltac2 plugin *) ] syn_level: [ @@ -2810,7 +2806,7 @@ syn_level: [ ] tac2def_syn: [ -| "Notation" LIST1 sexpr syn_level ":=" tac2expr6 (* Ltac2 plugin *) +| "Notation" LIST1 ltac2_scope syn_level ":=" ltac2_expr6 (* Ltac2 plugin *) ] lident: [ @@ -3028,28 +3024,28 @@ q_rewriting: [ ] G_LTAC2_tactic_then_last: [ -| "|" LIST0 ( OPT tac2expr6 ) SEP "|" (* Ltac2 plugin *) +| "|" LIST0 ( OPT ltac2_expr6 ) SEP "|" (* Ltac2 plugin *) | (* Ltac2 plugin *) ] -G_LTAC2_tactic_then_gen: [ -| tac2expr6 "|" G_LTAC2_tactic_then_gen (* Ltac2 plugin *) -| tac2expr6 ".." G_LTAC2_tactic_then_last (* Ltac2 plugin *) +G_LTAC2_for_each_goal: [ +| ltac2_expr6 "|" G_LTAC2_for_each_goal (* Ltac2 plugin *) +| ltac2_expr6 ".." G_LTAC2_tactic_then_last (* Ltac2 plugin *) | ".." G_LTAC2_tactic_then_last (* Ltac2 plugin *) -| tac2expr6 (* Ltac2 plugin *) -| "|" G_LTAC2_tactic_then_gen (* Ltac2 plugin *) +| ltac2_expr6 (* Ltac2 plugin *) +| "|" G_LTAC2_for_each_goal (* Ltac2 plugin *) | (* Ltac2 plugin *) ] q_dispatch: [ -| G_LTAC2_tactic_then_gen (* Ltac2 plugin *) +| G_LTAC2_for_each_goal (* Ltac2 plugin *) ] q_occurrences: [ | G_LTAC2_occs (* Ltac2 plugin *) ] -red_flag: [ +ltac2_red_flag: [ | "beta" (* Ltac2 plugin *) | "iota" (* Ltac2 plugin *) | "match" (* Ltac2 plugin *) @@ -3080,7 +3076,7 @@ G_LTAC2_delta_flag: [ ] G_LTAC2_strategy_flag: [ -| LIST1 red_flag (* Ltac2 plugin *) +| LIST1 ltac2_red_flag (* Ltac2 plugin *) | G_LTAC2_delta_flag (* Ltac2 plugin *) ] @@ -3098,12 +3094,12 @@ q_hintdb: [ ] G_LTAC2_match_pattern: [ -| "context" OPT Prim.ident "[" Constr.lconstr_pattern "]" (* Ltac2 plugin *) -| Constr.lconstr_pattern (* Ltac2 plugin *) +| "context" OPT Prim.ident "[" Constr.cpattern "]" (* Ltac2 plugin *) +| Constr.cpattern (* Ltac2 plugin *) ] G_LTAC2_match_rule: [ -| G_LTAC2_match_pattern "=>" tac2expr6 (* Ltac2 plugin *) +| G_LTAC2_match_pattern "=>" ltac2_expr6 (* Ltac2 plugin *) ] G_LTAC2_match_list: [ @@ -3124,16 +3120,16 @@ gmatch_pattern: [ ] gmatch_rule: [ -| gmatch_pattern "=>" tac2expr6 (* Ltac2 plugin *) +| gmatch_pattern "=>" ltac2_expr6 (* Ltac2 plugin *) ] -gmatch_list: [ +goal_match_list: [ | LIST1 gmatch_rule SEP "|" (* Ltac2 plugin *) | "|" LIST1 gmatch_rule SEP "|" (* Ltac2 plugin *) ] q_goal_matching: [ -| gmatch_list (* Ltac2 plugin *) +| goal_match_list (* Ltac2 plugin *) ] move_location: [ @@ -3167,7 +3163,7 @@ G_LTAC2_as_ipat: [ ] G_LTAC2_by_tactic: [ -| "by" tac2expr6 (* Ltac2 plugin *) +| "by" ltac2_expr6 (* Ltac2 plugin *) | (* Ltac2 plugin *) ] @@ -3190,11 +3186,11 @@ ltac2_entry: [ ] ltac2_expr: [ -| tac2expr6 (* Ltac2 plugin *) +| _ltac2_expr (* Ltac2 plugin *) ] tac2mode: [ -| ltac2_expr ltac_use_default (* Ltac2 plugin *) +| ltac2_expr6 ltac_use_default (* Ltac2 plugin *) | G_vernac.query_command (* Ltac2 plugin *) ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index ff1efa5375..12a7bc684d 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -320,11 +320,11 @@ univ_constraint: [ ] term_fix: [ -| "let" "fix" fix_body "in" term -| "fix" fix_body OPT ( LIST1 ( "with" fix_body ) "for" ident ) +| "let" "fix" fix_decl "in" term +| "fix" fix_decl OPT ( LIST1 ( "with" fix_decl ) "for" ident ) ] -fix_body: [ +fix_decl: [ | ident LIST0 binder OPT fixannot OPT ( ":" type ) ":=" term ] @@ -885,6 +885,7 @@ command: [ | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* ring plugin *) | "Print" "Fields" (* ring plugin *) | "Number" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier +| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident ) | "Typeclasses" "Transparent" LIST1 qualid | "Typeclasses" "Opaque" LIST1 qualid @@ -909,7 +910,6 @@ command: [ | "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family | "Declare" "Left" "Step" one_term | "Declare" "Right" "Step" one_term -| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier | "String" "Notation" qualid qualid qualid ":" scope_name | "SubClass" ident_decl def_body | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ] @@ -1435,7 +1435,7 @@ simple_tactic: [ | "notypeclasses" "refine" one_term | "simple" "notypeclasses" "refine" one_term | "solve_constraints" -| "subst" OPT ( LIST1 ident ) +| "subst" LIST0 ident | "simple" "subst" | "evar" "(" ident ":" term ")" | "evar" one_term diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index 297dc3a706..ddfa3a80bd 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -317,7 +317,7 @@ let pattern_of_string ?env s = | None -> Global.env () | Some e -> e in - let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in + let constr = Pcoq.parse_string Pcoq.Constr.cpattern s in let (_, pat) = Constrintern.intern_constr_pattern env (Evd.from_env env) constr in pat diff --git a/lib/genarg.mli b/lib/genarg.mli index 88e9ff13e8..aac43db672 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -11,7 +11,7 @@ (** Generic arguments used by the extension mechanisms of several Coq ASTs. *) (** The route of a generic argument, from parsing to evaluation. -In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc. +In the following diagram, "object" can be ltac_expr, constr, tactic_value, etc. {% \begin{verbatim} %} parsing in_raw out_raw diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 644493a010..349e14bba3 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -80,11 +80,11 @@ let test_array_closing = } GRAMMAR EXTEND Gram - GLOBAL: binder_constr lconstr constr operconstr + GLOBAL: binder_constr lconstr constr term universe_level universe_name sort sort_family - global constr_pattern lconstr_pattern Constr.ident + global constr_pattern cpattern Constr.ident closed_binder open_binders binder binders binders_fixannot - record_declaration typeclass_constraint pattern appl_arg type_cstr; + record_declaration typeclass_constraint pattern arg type_cstr; Constr.ident: [ [ id = Prim.ident -> { id } ] ] ; @@ -97,7 +97,7 @@ GRAMMAR EXTEND Gram constr_pattern: [ [ c = constr -> { c } ] ] ; - lconstr_pattern: + cpattern: [ [ c = lconstr -> { c } ] ] ; sort: @@ -131,48 +131,48 @@ GRAMMAR EXTEND Gram | u = universe_expr -> { [u] } ] ] ; lconstr: - [ [ c = operconstr LEVEL "200" -> { c } ] ] + [ [ c = term LEVEL "200" -> { c } ] ] ; constr: - [ [ c = operconstr LEVEL "8" -> { c } - | "@"; f=global; i = univ_instance -> { CAst.make ~loc @@ CAppExpl((None,f,i),[]) } ] ] + [ [ c = term LEVEL "8" -> { c } + | "@"; f=global; i = univ_annot -> { CAst.make ~loc @@ CAppExpl((None,f,i),[]) } ] ] ; - operconstr: + term: [ "200" RIGHTA [ c = binder_constr -> { c } ] | "100" RIGHTA - [ c1 = operconstr; "<:"; c2 = operconstr LEVEL "200" -> + [ c1 = term; "<:"; c2 = term LEVEL "200" -> { CAst.make ~loc @@ CCast(c1, CastVM c2) } - | c1 = operconstr; "<<:"; c2 = operconstr LEVEL "200" -> + | c1 = term; "<<:"; c2 = term LEVEL "200" -> { CAst.make ~loc @@ CCast(c1, CastNative c2) } - | c1 = operconstr; ":"; c2 = operconstr LEVEL "200" -> + | c1 = term; ":"; c2 = term LEVEL "200" -> { CAst.make ~loc @@ CCast(c1, CastConv c2) } - | c1 = operconstr; ":>" -> + | c1 = term; ":>" -> { CAst.make ~loc @@ CCast(c1, CastCoerce) } ] | "99" RIGHTA [ ] | "90" RIGHTA [ ] | "10" LEFTA - [ f = operconstr; args = LIST1 appl_arg -> { CAst.make ~loc @@ CApp((None,f),args) } - | "@"; f = global; i = univ_instance; args = LIST0 NEXT -> { CAst.make ~loc @@ CAppExpl((None,f,i),args) } + [ f = term; args = LIST1 arg -> { CAst.make ~loc @@ CApp((None,f),args) } + | "@"; f = global; i = univ_annot; args = LIST0 NEXT -> { CAst.make ~loc @@ CAppExpl((None,f,i),args) } | "@"; lid = pattern_ident; args = LIST1 identref -> { let { CAst.loc = locid; v = id } = lid in let args = List.map (fun x -> CAst.make @@ CRef (qualid_of_ident ?loc:x.CAst.loc x.CAst.v, None), None) args in CAst.make ~loc @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) } ] | "9" - [ ".."; c = operconstr LEVEL "0"; ".." -> + [ ".."; c = term LEVEL "0"; ".." -> { CAst.make ~loc @@ CAppExpl ((None, (qualid_of_ident ~loc ldots_var), None),[c]) } ] | "8" [ ] | "1" LEFTA - [ c = operconstr; ".("; f = global; args = LIST0 appl_arg; ")" -> + [ c = term; ".("; f = global; args = LIST0 arg; ")" -> { CAst.make ~loc @@ CApp((Some (List.length args+1), CAst.make @@ CRef (f,None)),args@[c,None]) } - | c = operconstr; ".("; "@"; f = global; - args = LIST0 (operconstr LEVEL "9"); ")" -> + | c = term; ".("; "@"; f = global; + args = LIST0 (term LEVEL "9"); ")" -> { CAst.make ~loc @@ CAppExpl((Some (List.length args+1),f,None),args@[c]) } - | c = operconstr; "%"; key = IDENT -> { CAst.make ~loc @@ CDelimiters (key,c) } ] + | c = term; "%"; key = IDENT -> { CAst.make ~loc @@ CDelimiters (key,c) } ] | "0" [ c = atomic_constr -> { c } - | c = match_constr -> { c } - | "("; c = operconstr LEVEL "200"; ")" -> + | c = term_match -> { c } + | "("; c = term LEVEL "200"; ")" -> { (* Preserve parentheses around numerals so that constrintern does not collapse -(3) into the numeral -3. *) (match c.CAst.v with @@ -182,14 +182,14 @@ GRAMMAR EXTEND Gram | "{|"; c = record_declaration; bar_cbrace -> { c } | "{"; c = binder_constr ; "}" -> { CAst.make ~loc @@ CNotation(None,(InConstrEntry,"{ _ }"),([c],[],[],[])) } - | "`{"; c = operconstr LEVEL "200"; "}" -> + | "`{"; c = term LEVEL "200"; "}" -> { CAst.make ~loc @@ CGeneralization (MaxImplicit, None, c) } - | test_array_opening; "["; "|"; ls = array_elems; "|"; def = lconstr; ty = type_cstr; test_array_closing; "|"; "]"; u = univ_instance -> + | test_array_opening; "["; "|"; ls = array_elems; "|"; def = lconstr; ty = type_cstr; test_array_closing; "|"; "]"; u = univ_annot -> { let t = Array.make (List.length ls) def in List.iteri (fun i e -> t.(i) <- e) ls; CAst.make ~loc @@ CArray(u, t, def, ty) } - | "`("; c = operconstr LEVEL "200"; ")" -> + | "`("; c = term LEVEL "200"; ")" -> { CAst.make ~loc @@ CGeneralization (Explicit, None, c) } ] ] ; array_elems: @@ -208,55 +208,55 @@ GRAMMAR EXTEND Gram { (id, mkLambdaCN ~loc bl c) } ] ] ; binder_constr: - [ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" -> + [ [ "forall"; bl = open_binders; ","; c = term LEVEL "200" -> { mkProdCN ~loc bl c } - | "fun"; bl = open_binders; "=>"; c = operconstr LEVEL "200" -> + | "fun"; bl = open_binders; "=>"; c = term LEVEL "200" -> { mkLambdaCN ~loc bl c } | "let"; id=name; bl = binders; ty = let_type_cstr; ":="; - c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> + c1 = term LEVEL "200"; "in"; c2 = term LEVEL "200" -> { let ty,c1 = match ty, c1 with | (_,None), { CAst.v = CCast(c, CastConv t) } -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *) | _, _ -> ty, c1 in CAst.make ~loc @@ CLetIn(id,mkLambdaCN ?loc:(constr_loc c1) bl c1, Option.map (mkProdCN ?loc:(fst ty) bl) (snd ty), c2) } - | "let"; "fix"; fx = fix_decl; "in"; c = operconstr LEVEL "200" -> + | "let"; "fix"; fx = fix_decl; "in"; c = term LEVEL "200" -> { let {CAst.loc=locf;CAst.v=({CAst.loc=li;CAst.v=id} as lid,_,_,_,_ as dcl)} = fx in let fix = CAst.make ?loc:locf @@ CFix (lid,[dcl]) in CAst.make ~loc @@ CLetIn( CAst.make ?loc:li @@ Name id,fix,None,c) } - | "let"; "cofix"; fx = cofix_decl; "in"; c = operconstr LEVEL "200" -> + | "let"; "cofix"; fx = cofix_body; "in"; c = term LEVEL "200" -> { let {CAst.loc=locf;CAst.v=({CAst.loc=li;CAst.v=id} as lid,_,_,_ as dcl)} = fx in let cofix = CAst.make ?loc:locf @@ CCoFix (lid,[dcl]) in CAst.make ~loc @@ CLetIn( CAst.make ?loc:li @@ Name id,cofix,None,c) } | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> { l } | "()" -> { [] } ]; - po = return_type; ":="; c1 = operconstr LEVEL "200"; "in"; - c2 = operconstr LEVEL "200" -> + po = as_return_type; ":="; c1 = term LEVEL "200"; "in"; + c2 = term LEVEL "200" -> { CAst.make ~loc @@ CLetTuple (lb,po,c1,c2) } - | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; - "in"; c2 = operconstr LEVEL "200" -> + | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = term LEVEL "200"; + "in"; c2 = term LEVEL "200" -> { CAst.make ~loc @@ CCases (LetPatternStyle, None, [c1, None, None], [CAst.make ~loc ([[p]], c2)]) } - | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; - rt = case_type; "in"; c2 = operconstr LEVEL "200" -> + | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = term LEVEL "200"; + rt = case_type; "in"; c2 = term LEVEL "200" -> { CAst.make ~loc @@ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [CAst.make ~loc ([[p]], c2)]) } | "let"; "'"; p = pattern LEVEL "200"; "in"; t = pattern LEVEL "200"; - ":="; c1 = operconstr LEVEL "200"; rt = case_type; - "in"; c2 = operconstr LEVEL "200" -> + ":="; c1 = term LEVEL "200"; rt = case_type; + "in"; c2 = term LEVEL "200" -> { CAst.make ~loc @@ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [CAst.make ~loc ([[p]], c2)]) } - | "if"; c = operconstr LEVEL "200"; po = return_type; - "then"; b1 = operconstr LEVEL "200"; - "else"; b2 = operconstr LEVEL "200" -> + | "if"; c = term LEVEL "200"; po = as_return_type; + "then"; b1 = term LEVEL "200"; + "else"; b2 = term LEVEL "200" -> { CAst.make ~loc @@ CIf (c, po, b1, b2) } | "fix"; c = fix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CFix (id,dcls) } | "cofix"; c = cofix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CCoFix (id,dcls) } ] ] ; - appl_arg: + arg: [ [ test_lpar_id_coloneq; "("; id = identref; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ?loc:id.CAst.loc @@ ExplByName id.CAst.v)) } - | c=operconstr LEVEL "9" -> { (c,None) } ] ] + | c=term LEVEL "9" -> { (c,None) } ] ] ; atomic_constr: - [ [ g = global; i = univ_instance -> { CAst.make ~loc @@ CRef (g,i) } + [ [ g = global; i = univ_annot -> { CAst.make ~loc @@ CRef (g,i) } | s = sort -> { CAst.make ~loc @@ CSort s } | n = NUMBER-> { CAst.make ~loc @@ CPrim (Numeral (NumTok.SPlus,n)) } | s = string -> { CAst.make ~loc @@ CPrim (String s) } @@ -272,7 +272,7 @@ GRAMMAR EXTEND Gram [ [ "@{"; l = LIST1 inst SEP ";"; "}" -> { l } | -> { [] } ] ] ; - univ_instance: + univ_annot: [ [ "@{"; l = LIST0 universe_level; "}" -> { Some l } | -> { None } ] ] ; @@ -290,34 +290,34 @@ GRAMMAR EXTEND Gram { (id,List.map (fun x -> x.CAst.v) (dcl::dcls)) } ] ] ; cofix_decls: - [ [ dcl = cofix_decl -> { let (id,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) } - | dcl = cofix_decl; "with"; dcls = LIST1 cofix_decl SEP "with"; "for"; id = identref -> + [ [ dcl = cofix_body -> { let (id,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) } + | dcl = cofix_body; "with"; dcls = LIST1 cofix_body SEP "with"; "for"; id = identref -> { (id,List.map (fun x -> x.CAst.v) (dcl::dcls)) } ] ] ; fix_decl: [ [ id = identref; bl = binders_fixannot; ty = type_cstr; ":="; - c = operconstr LEVEL "200" -> + c = term LEVEL "200" -> { CAst.make ~loc (id,snd bl,fst bl,ty,c) } ] ] ; - cofix_decl: + cofix_body: [ [ id = identref; bl = binders; ty = type_cstr; ":="; - c = operconstr LEVEL "200" -> + c = term LEVEL "200" -> { CAst.make ~loc (id,bl,ty,c) } ] ] ; - match_constr: + term_match: [ [ "match"; ci = LIST1 case_item SEP ","; ty = OPT case_type; "with"; br = branches; "end" -> { CAst.make ~loc @@ CCases(RegularStyle,ty,ci,br) } ] ] ; case_item: - [ [ c = operconstr LEVEL "100"; + [ [ c = term LEVEL "100"; ona = OPT ["as"; id = name -> { id } ]; ty = OPT ["in"; t = pattern LEVEL "200" -> { t } ] -> { (c,ona,ty) } ] ] ; case_type: - [ [ "return"; ty = operconstr LEVEL "100" -> { ty } ] ] + [ [ "return"; ty = term LEVEL "100" -> { ty } ] ] ; - return_type: + as_return_type: [ [ a = OPT [ na = OPT["as"; na = name -> { na } ]; ty = case_type -> { (na,ty) } ] -> { match a with @@ -345,7 +345,7 @@ GRAMMAR EXTEND Gram pattern: [ "200" RIGHTA [ ] | "100" RIGHTA - [ p = pattern; ":"; ty = operconstr LEVEL "200" -> + [ p = pattern; ":"; ty = term LEVEL "200" -> { CAst.make ~loc @@ CPatCast (p, ty) } ] | "99" RIGHTA [ ] | "90" RIGHTA [ ] @@ -447,12 +447,12 @@ GRAMMAR EXTEND Gram [CLocalPattern (CAst.make ~loc (p, ty))] } ] ] ; typeclass_constraint: - [ [ "!" ; c = operconstr LEVEL "200" -> { (CAst.make ~loc Anonymous), true, c } - | "{"; id = name; "}"; ":" ; expl = [ "!" -> { true } | -> { false } ] ; c = operconstr LEVEL "200" -> + [ [ "!" ; c = term LEVEL "200" -> { (CAst.make ~loc Anonymous), true, c } + | "{"; id = name; "}"; ":" ; expl = [ "!" -> { true } | -> { false } ] ; c = term LEVEL "200" -> { id, expl, c } - | test_name_colon; iid = name; ":" ; expl = [ "!" -> { true } | -> { false } ] ; c = operconstr LEVEL "200" -> + | test_name_colon; iid = name; ":" ; expl = [ "!" -> { true } | -> { false } ] ; c = term LEVEL "200" -> { iid, expl, c } - | c = operconstr LEVEL "200" -> + | c = term LEVEL "200" -> { (CAst.make ~loc Anonymous), false, c } ] ] ; type_cstr: diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 996aa0925c..22b5e70311 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -308,7 +308,8 @@ module Constr = (* Entries that can be referred via the string -> Entry.t table *) let constr = Entry.create "constr" - let operconstr = Entry.create "operconstr" + let term = Entry.create "term" + let operconstr = term let constr_eoi = eoi_entry constr let lconstr = Entry.create "lconstr" let binder_constr = Entry.create "binder_constr" @@ -320,7 +321,8 @@ module Constr = let sort_family = Entry.create "sort_family" let pattern = Entry.create "pattern" let constr_pattern = Entry.create "constr_pattern" - let lconstr_pattern = Entry.create "lconstr_pattern" + let cpattern = Entry.create "cpattern" + let lconstr_pattern = cpattern let closed_binder = Entry.create "closed_binder" let binder = Entry.create "binder" let binders = Entry.create "binders" @@ -328,7 +330,8 @@ module Constr = let binders_fixannot = Entry.create "binders_fixannot" let typeclass_constraint = Entry.create "typeclass_constraint" let record_declaration = Entry.create "record_declaration" - let appl_arg = Entry.create "appl_arg" + let arg = Entry.create "arg" + let appl_arg = arg let type_cstr = Entry.create "type_cstr" end diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 8e60bbf504..ce4c91d51f 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -185,7 +185,9 @@ module Constr : val constr_eoi : constr_expr Entry.t val lconstr : constr_expr Entry.t val binder_constr : constr_expr Entry.t + val term : constr_expr Entry.t val operconstr : constr_expr Entry.t + [@@deprecated "Deprecated in 8.13; use 'term' instead"] val ident : Id.t Entry.t val global : qualid Entry.t val universe_name : Glob_term.glob_sort_name Entry.t @@ -194,7 +196,9 @@ module Constr : val sort_family : Sorts.family Entry.t val pattern : cases_pattern_expr Entry.t val constr_pattern : constr_expr Entry.t + val cpattern : constr_expr Entry.t val lconstr_pattern : constr_expr Entry.t + [@@deprecated "Deprecated in 8.13; use 'cpattern' instead"] val closed_binder : local_binder_expr list Entry.t val binder : local_binder_expr list Entry.t (* closed_binder or variable *) val binders : local_binder_expr list Entry.t (* list of binder *) @@ -202,7 +206,9 @@ module Constr : val binders_fixannot : (local_binder_expr list * recursion_order_expr option) Entry.t val typeclass_constraint : (lname * bool * constr_expr) Entry.t val record_declaration : constr_expr Entry.t + val arg : (constr_expr * explicitation CAst.t option) Entry.t val appl_arg : (constr_expr * explicitation CAst.t option) Entry.t + [@@deprecated "Deprecated in 8.13; use 'arg' instead"] val type_cstr : constr_expr Entry.t end diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index bbc4df7dde..ca6ae150a7 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -147,19 +147,19 @@ END module Vernac = Pvernac.Vernac_ module Tactic = Pltac -let (wit_function_rec_definition_loc : Vernacexpr.fixpoint_expr Loc.located Genarg.uniform_genarg_type) = - Genarg.create_arg "function_rec_definition_loc" +let (wit_function_fix_definition : Vernacexpr.fixpoint_expr Loc.located Genarg.uniform_genarg_type) = + Genarg.create_arg "function_fix_definition" -let function_rec_definition_loc = - Pcoq.create_generic_entry2 "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc) +let function_fix_definition = + Pcoq.create_generic_entry2 "function_fix_definition" (Genarg.rawwit wit_function_fix_definition) } GRAMMAR EXTEND Gram - GLOBAL: function_rec_definition_loc ; + GLOBAL: function_fix_definition ; - function_rec_definition_loc: - [ [ g = Vernac.rec_definition -> { Loc.tag ~loc g } ]] + function_fix_definition: + [ [ g = Vernac.fix_definition -> { Loc.tag ~loc g } ]] ; END @@ -168,7 +168,7 @@ END let () = let raw_printer env sigma _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in - Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer + Pptactic.declare_extra_vernac_genarg_pprule wit_function_fix_definition raw_printer let is_proof_termination_interactively_checked recsl = List.exists (function @@ -196,7 +196,7 @@ let is_interactive recsl = } VERNAC COMMAND EXTEND Function STATE CUSTOM -| ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] +| ["Function" ne_function_fix_definition_list_sep(recsl,"with")] => { classify_funind recsl } -> { if is_interactive recsl then diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index ad4374dba3..ff4a82f864 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -41,7 +41,7 @@ let () = create_generic_quotation "ipattern" Pltac.simple_intropattern wit_simpl let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Stdarg.wit_open_constr let () = let inject (loc, v) = Tacexpr.Tacexp v in - Tacentries.create_ltac_quotation "ltac" inject (Pltac.tactic_expr, Some 5) + Tacentries.create_ltac_quotation "ltac" inject (Pltac.ltac_expr, Some 5) (** Backward-compatible tactic notation entry names *) diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 2d74323689..c38a4dcd90 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -74,22 +74,22 @@ let hint = G_proofs.hint } GRAMMAR EXTEND Gram - GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint + GLOBAL: tactic tacdef_body ltac_expr binder_tactic tactic_value command hint tactic_mode constr_may_eval constr_eval toplevel_selector - operconstr; + term; tactic_then_last: - [ [ "|"; lta = LIST0 (OPT tactic_expr) SEP "|" -> + [ [ "|"; lta = LIST0 (OPT ltac_expr) SEP "|" -> { Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta) } | -> { [||] } ] ] ; - tactic_then_gen: - [ [ ta = tactic_expr; "|"; tg = tactic_then_gen -> { let (first,last) = tg in (ta::first, last) } - | ta = tactic_expr; ".."; l = tactic_then_last -> { ([], Some (ta, l)) } + for_each_goal: + [ [ ta = ltac_expr; "|"; tg = for_each_goal -> { let (first,last) = tg in (ta::first, last) } + | ta = ltac_expr; ".."; l = tactic_then_last -> { ([], Some (ta, l)) } | ".."; l = tactic_then_last -> { ([], Some (TacId [], l)) } - | ta = tactic_expr -> { ([ta], None) } - | "|"; tg = tactic_then_gen -> { let (first,last) = tg in (TacId [] :: first, last) } + | ta = ltac_expr -> { ([ta], None) } + | "|"; tg = for_each_goal -> { let (first,last) = tg in (TacId [] :: first, last) } | -> { ([TacId []], None) } ] ] ; @@ -97,13 +97,13 @@ GRAMMAR EXTEND Gram for [TacExtend] *) [ [ "[" ; l = OPT">" -> { if Option.is_empty l then true else false } ] ] ; - tactic_expr: + ltac_expr: [ "5" RIGHTA [ te = binder_tactic -> { te } ] | "4" LEFTA - [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> { TacThen (ta0, ta1) } - | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> { TacThen (ta0,ta1) } - | ta0 = tactic_expr; ";"; l = tactic_then_locality; tg = tactic_then_gen; "]" -> { + [ ta0 = ltac_expr; ";"; ta1 = binder_tactic -> { TacThen (ta0, ta1) } + | ta0 = ltac_expr; ";"; ta1 = ltac_expr -> { TacThen (ta0,ta1) } + | ta0 = ltac_expr; ";"; l = tactic_then_locality; tg = for_each_goal; "]" -> { let (first,tail) = tg in match l , tail with | false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last)) @@ -111,51 +111,51 @@ GRAMMAR EXTEND Gram | false , None -> TacThen (ta0,TacDispatch first) | true , None -> TacThens (ta0,first) } ] | "3" RIGHTA - [ IDENT "try"; ta = tactic_expr -> { TacTry ta } - | IDENT "do"; n = int_or_var; ta = tactic_expr -> { TacDo (n,ta) } - | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> { TacTimeout (n,ta) } - | IDENT "time"; s = OPT string; ta = tactic_expr -> { TacTime (s,ta) } - | IDENT "repeat"; ta = tactic_expr -> { TacRepeat ta } - | IDENT "progress"; ta = tactic_expr -> { TacProgress ta } - | IDENT "once"; ta = tactic_expr -> { TacOnce ta } - | IDENT "exactly_once"; ta = tactic_expr -> { TacExactlyOnce ta } - | IDENT "infoH"; ta = tactic_expr -> { TacShowHyps ta } + [ IDENT "try"; ta = ltac_expr -> { TacTry ta } + | IDENT "do"; n = int_or_var; ta = ltac_expr -> { TacDo (n,ta) } + | IDENT "timeout"; n = int_or_var; ta = ltac_expr -> { TacTimeout (n,ta) } + | IDENT "time"; s = OPT string; ta = ltac_expr -> { TacTime (s,ta) } + | IDENT "repeat"; ta = ltac_expr -> { TacRepeat ta } + | IDENT "progress"; ta = ltac_expr -> { TacProgress ta } + | IDENT "once"; ta = ltac_expr -> { TacOnce ta } + | IDENT "exactly_once"; ta = ltac_expr -> { TacExactlyOnce ta } + | IDENT "infoH"; ta = ltac_expr -> { TacShowHyps ta } (*To do: put Abstract in Refiner*) | IDENT "abstract"; tc = NEXT -> { TacAbstract (tc,None) } | IDENT "abstract"; tc = NEXT; "using"; s = ident -> { TacAbstract (tc,Some s) } - | sel = selector; ta = tactic_expr -> { TacSelect (sel, ta) } ] + | IDENT "only"; sel = selector; ":"; ta = ltac_expr -> { TacSelect (sel, ta) } ] (*End of To do*) | "2" RIGHTA - [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> { TacOr (ta0,ta1) } - | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> { TacOr (ta0,ta1) } - | IDENT "tryif" ; ta = tactic_expr ; - "then" ; tat = tactic_expr ; - "else" ; tae = tactic_expr -> { TacIfThenCatch(ta,tat,tae) } - | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> { TacOrelse (ta0,ta1) } - | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> { TacOrelse (ta0,ta1) } ] + [ ta0 = ltac_expr; "+"; ta1 = binder_tactic -> { TacOr (ta0,ta1) } + | ta0 = ltac_expr; "+"; ta1 = ltac_expr -> { TacOr (ta0,ta1) } + | IDENT "tryif" ; ta = ltac_expr ; + "then" ; tat = ltac_expr ; + "else" ; tae = ltac_expr -> { TacIfThenCatch(ta,tat,tae) } + | ta0 = ltac_expr; "||"; ta1 = binder_tactic -> { TacOrelse (ta0,ta1) } + | ta0 = ltac_expr; "||"; ta1 = ltac_expr -> { TacOrelse (ta0,ta1) } ] | "1" RIGHTA [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" -> { TacMatchGoal (b,false,mrl) } | b = match_key; IDENT "reverse"; IDENT "goal"; "with"; mrl = match_context_list; "end" -> { TacMatchGoal (b,true,mrl) } - | b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" -> + | b = match_key; c = ltac_expr; "with"; mrl = match_list; "end" -> { TacMatch (b,c,mrl) } - | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> + | IDENT "first" ; "["; l = LIST0 ltac_expr SEP "|"; "]" -> { TacFirst l } - | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> + | IDENT "solve" ; "["; l = LIST0 ltac_expr SEP "|"; "]" -> { TacSolve l } | IDENT "idtac"; l = LIST0 message_token -> { TacId l } | g=failkw; n = [ n = int_or_var -> { n } | -> { fail_default_value } ]; l = LIST0 message_token -> { TacFail (g,n,l) } | st = simple_tactic -> { st } - | a = tactic_arg -> { TacArg(CAst.make ~loc a) } - | r = reference; la = LIST0 tactic_arg_compat -> + | a = tactic_value -> { TacArg(CAst.make ~loc a) } + | r = reference; la = LIST0 tactic_arg -> { TacArg(CAst.make ~loc @@ TacCall (CAst.make ~loc (r,la))) } ] | "0" - [ "("; a = tactic_expr; ")" -> { a } - | "["; ">"; tg = tactic_then_gen; "]" -> { + [ "("; a = ltac_expr; ")" -> { a } + | "["; ">"; tg = for_each_goal; "]" -> { let (tf,tail) = tg in begin match tail with | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl) @@ -166,24 +166,24 @@ GRAMMAR EXTEND Gram failkw: [ [ IDENT "fail" -> { TacLocal } | IDENT "gfail" -> { TacGlobal } ] ] ; - (* binder_tactic: level 5 of tactic_expr *) + (* binder_tactic: level 5 of ltac_expr *) binder_tactic: [ RIGHTA - [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" -> + [ "fun"; it = LIST1 input_fun ; "=>"; body = ltac_expr LEVEL "5" -> { TacFun (it,body) } | "let"; isrec = [IDENT "rec" -> { true } | -> { false } ]; llc = LIST1 let_clause SEP "with"; "in"; - body = tactic_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) } ] ] + body = ltac_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) } ] ] ; (* Tactic arguments to the right of an application *) - tactic_arg_compat: - [ [ a = tactic_arg -> { a } + tactic_arg: + [ [ a = tactic_value -> { a } | c = Constr.constr -> { (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c)) } (* Unambiguous entries: tolerated w/o "ltac:" modifier *) | "()" -> { TacGeneric (None, genarg_of_unit ()) } ] ] ; (* Can be used as argument and at toplevel in tactic expressions. *) - tactic_arg: + tactic_value: [ [ c = constr_eval -> { ConstrMayEval c } | IDENT "fresh"; l = LIST0 fresh_id -> { TacFreshId l } | IDENT "type_term"; c=uconstr -> { TacPretype c } @@ -223,20 +223,20 @@ GRAMMAR EXTEND Gram | l = ident -> { Name.Name l } ] ] ; let_clause: - [ [ idr = identref; ":="; te = tactic_expr -> + [ [ idr = identref; ":="; te = ltac_expr -> { (CAst.map (fun id -> Name id) idr, arg_of_expr te) } - | na = ["_" -> { CAst.make ~loc Anonymous } ]; ":="; te = tactic_expr -> + | na = ["_" -> { CAst.make ~loc Anonymous } ]; ":="; te = ltac_expr -> { (na, arg_of_expr te) } - | idr = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> + | idr = identref; args = LIST1 input_fun; ":="; te = ltac_expr -> { (CAst.map (fun id -> Name id) idr, arg_of_expr (TacFun(args,te))) } ] ] ; match_pattern: [ [ IDENT "context"; oid = OPT Constr.ident; - "["; pc = Constr.lconstr_pattern; "]" -> + "["; pc = Constr.cpattern; "]" -> { Subterm (oid, pc) } - | pc = Constr.lconstr_pattern -> { Term pc } ] ] + | pc = Constr.cpattern -> { Term pc } ] ] ; - match_hyps: + match_hyp: [ [ na = name; ":"; mp = match_pattern -> { Hyp (na, mp) } | na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> { Def (na, mpv, mpt) } | na = name; ":="; mpv = match_pattern -> @@ -250,19 +250,19 @@ GRAMMAR EXTEND Gram ] ] ; match_context_rule: - [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; - "=>"; te = tactic_expr -> { Pat (largs, mp, te) } - | "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; - "]"; "=>"; te = tactic_expr -> { Pat (largs, mp, te) } - | "_"; "=>"; te = tactic_expr -> { All te } ] ] + [ [ largs = LIST0 match_hyp SEP ","; "|-"; mp = match_pattern; + "=>"; te = ltac_expr -> { Pat (largs, mp, te) } + | "["; largs = LIST0 match_hyp SEP ","; "|-"; mp = match_pattern; + "]"; "=>"; te = ltac_expr -> { Pat (largs, mp, te) } + | "_"; "=>"; te = ltac_expr -> { All te } ] ] ; match_context_list: [ [ mrl = LIST1 match_context_rule SEP "|" -> { mrl } | "|"; mrl = LIST1 match_context_rule SEP "|" -> { mrl } ] ] ; match_rule: - [ [ mp = match_pattern; "=>"; te = tactic_expr -> { Pat ([],mp,te) } - | "_"; "=>"; te = tactic_expr -> { All te } ] ] + [ [ mp = match_pattern; "=>"; te = ltac_expr -> { Pat ([],mp,te) } + | "_"; "=>"; te = ltac_expr -> { All te } ] ] ; match_list: [ [ mrl = LIST1 match_rule SEP "|" -> { mrl } @@ -282,13 +282,13 @@ GRAMMAR EXTEND Gram (* Definitions for tactics *) tacdef_body: [ [ name = Constr.global; it=LIST1 input_fun; - redef = ltac_def_kind; body = tactic_expr -> + redef = ltac_def_kind; body = ltac_expr -> { if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body)) else let id = reference_to_id name in Tacexpr.TacticDefinition (id, TacFun (it, body)) } | name = Constr.global; redef = ltac_def_kind; - body = tactic_expr -> + body = ltac_expr -> { if redef then Tacexpr.TacticRedefinition (name, body) else let id = reference_to_id name in @@ -296,7 +296,7 @@ GRAMMAR EXTEND Gram ] ] ; tactic: - [ [ tac = tactic_expr -> { tac } ] ] + [ [ tac = ltac_expr -> { tac } ] ] ; range_selector: @@ -314,15 +314,12 @@ GRAMMAR EXTEND Gram { let open Goal_select in Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l } ] ] ; - selector_body: + selector: [ [ l = range_selector_or_nth -> { l } | test_bracket_ident; "["; id = ident; "]" -> { Goal_select.SelectId id } ] ] ; - selector: - [ [ IDENT "only"; sel = selector_body; ":" -> { sel } ] ] - ; toplevel_selector: - [ [ sel = selector_body; ":" -> { sel } + [ [ sel = selector; ":" -> { sel } | "!"; ":" -> { Goal_select.SelectAlreadyFocused } | IDENT "all"; ":" -> { Goal_select.SelectAll } ] ] ; @@ -343,8 +340,8 @@ GRAMMAR EXTEND Gram tac = Pltac.tactic -> { Vernacexpr.HintsExtern (n,c, in_tac tac) } ] ] ; - operconstr: LEVEL "0" - [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" -> + term: LEVEL "0" + [ [ IDENT "ltac"; ":"; "("; tac = Pltac.ltac_expr; ")" -> { let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in CAst.make ~loc @@ CHole (None, IntroAnonymous, Some arg) } ] ] ; diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index c186a83a5c..97d75261c5 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -291,7 +291,7 @@ GRAMMAR EXTEND Gram ; simple_intropattern: [ [ pat = simple_intropattern_closed; - l = LIST0 ["%"; c = operconstr LEVEL "0" -> { c } ] -> + l = LIST0 ["%"; c = term LEVEL "0" -> { c } ] -> { let {CAst.loc=loc0;v=pat} = pat in let f c pat = let loc1 = Constrexpr_ops.constr_loc c in @@ -320,7 +320,7 @@ GRAMMAR EXTEND Gram with_bindings: [ [ "with"; bl = bindings -> { bl } | -> { NoBindings } ] ] ; - red_flags: + red_flag: [ [ IDENT "beta" -> { [FBeta] } | IDENT "iota" -> { [FMatch;FFix;FCofix] } | IDENT "match" -> { [FMatch] } @@ -337,7 +337,7 @@ GRAMMAR EXTEND Gram ] ] ; strategy_flag: - [ [ s = LIST1 red_flags -> { Redops.make_red_flag (List.flatten s) } + [ [ s = LIST1 red_flag -> { Redops.make_red_flag (List.flatten s) } | d = delta_flag -> { all_with d } ] ] ; @@ -460,7 +460,7 @@ GRAMMAR EXTEND Gram [ [ "as"; id = ident -> { Names.Name.Name id } | -> { Names.Name.Anonymous } ] ] ; by_tactic: - [ [ "by"; tac = tactic_expr LEVEL "3" -> { Some tac } + [ [ "by"; tac = ltac_expr LEVEL "3" -> { Some tac } | -> { None } ] ] ; rewriter : diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index b7b54143df..94e398fe5d 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -37,8 +37,10 @@ let clause_dft_concl = (* Main entries for ltac *) -let tactic_arg = Entry.create "tactic_arg" -let tactic_expr = Entry.create "tactic_expr" +let tactic_value = Entry.create "tactic_value" +let tactic_arg = tactic_value +let ltac_expr = Entry.create "ltac_expr" +let tactic_expr = ltac_expr let binder_tactic = Entry.create "binder_tactic" let tactic = Entry.create "tactic" diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 8565c4b4d6..3a4a081c93 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -31,8 +31,12 @@ val simple_tactic : raw_tactic_expr Entry.t val simple_intropattern : constr_expr intro_pattern_expr CAst.t Entry.t 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 tactic_arg : raw_tactic_arg Entry.t + [@@deprecated "Deprecated in 8.13; use 'tactic_value' instead"] +val ltac_expr : raw_tactic_expr Entry.t val tactic_expr : raw_tactic_expr Entry.t + [@@deprecated "Deprecated in 8.13; use 'ltac_expr' instead"] 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/pptactic.mli b/plugins/ltac/pptactic.mli index 6a9fb5c2ea..5e199dad62 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** This module implements pretty-printers for tactic_expr syntactic +(** This module implements pretty-printers for ltac_expr syntactic objects and their subcomponents. *) open Genarg diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 6823b6411f..a05b36c1b4 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -33,7 +33,7 @@ type argument = Genarg.ArgT.any Extend.user_symbol let atactic n = if n = 5 then Pcoq.Symbol.nterm Pltac.binder_tactic - else Pcoq.Symbol.nterml Pltac.tactic_expr (string_of_int n) + else 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 @@ -116,7 +116,7 @@ let get_tactic_entry n = else if Int.equal n 5 then Pltac.binder_tactic, None else if 1<=n && n<5 then - Pltac.tactic_expr, Some (Gramlib.Gramext.Level (string_of_int n)) + Pltac.ltac_expr, Some (Gramlib.Gramext.Level (string_of_int n)) else user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^".")) @@ -383,7 +383,7 @@ let add_ml_tactic_notation name ~level ?deprecation prods = in List.iteri iter (List.rev prods); (* We call [extend_atomic_tactic] only for "basic tactics" (the ones - at tactic_expr level 0) *) + at ltac_expr level 0) *) if Int.equal level 0 then extend_atomic_tactic name prods (**********************************************************************) @@ -420,7 +420,7 @@ let create_ltac_quotation name cast (e, l) = in let action _ v _ _ _ loc = cast (Some loc, v) in let gram = (level, assoc, [Pcoq.Production.make rule action]) in - Pcoq.grammar_extend Pltac.tactic_arg {pos=None; data=[gram]} + Pcoq.grammar_extend Pltac.tactic_value {pos=None; data=[gram]} (** Command *) @@ -555,10 +555,10 @@ let print_located_tactic qid = let () = let entries = [ - AnyEntry Pltac.tactic_expr; + AnyEntry Pltac.ltac_expr; AnyEntry Pltac.binder_tactic; AnyEntry Pltac.simple_tactic; - AnyEntry Pltac.tactic_arg; + AnyEntry Pltac.tactic_value; ] in register_grammars_by_name "tactic" entries diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 22b9abda20..7728415ddd 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1997,7 +1997,7 @@ let interp_tac_gen lfun avoid_ids debug t = let interp t = interp_tac_gen Id.Map.empty Id.Set.empty (get_debug()) t (* MUST be marshallable! *) -type tactic_expr = { +type ltac_expr = { global: bool; ast: Tacexpr.raw_tactic_expr; } diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index dba9c938ec..fe3079198c 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -126,12 +126,12 @@ val interp_tac_gen : value Id.Map.t -> Id.Set.t -> val interp : raw_tactic_expr -> unit Proofview.tactic (** Hides interpretation for pretty-print *) -type tactic_expr = { +type ltac_expr = { global: bool; ast: Tacexpr.raw_tactic_expr; } -val hide_interp : tactic_expr -> ComTactic.interpretable +val hide_interp : ltac_expr -> ComTactic.interpretable (** Internals that can be useful for syntax extensions. *) diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 7b584b5159..70dab585bf 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -100,7 +100,7 @@ ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma } END GRAMMAR EXTEND Gram GLOBAL: ssrtacarg; - ssrtacarg: [[ tac = tactic_expr LEVEL "5" -> { tac } ]]; + ssrtacarg: [[ tac = ltac_expr LEVEL "5" -> { tac } ]]; END (* Copy of ssrtacarg with LEVEL "3", useful for: "under ... do ..." *) @@ -108,7 +108,7 @@ ARGUMENT EXTEND ssrtac3arg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma } END GRAMMAR EXTEND Gram GLOBAL: ssrtac3arg; - ssrtac3arg: [[ tac = tactic_expr LEVEL "3" -> { tac } ]]; + ssrtac3arg: [[ tac = ltac_expr LEVEL "3" -> { tac } ]]; END { @@ -1337,7 +1337,7 @@ ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinde GRAMMAR EXTEND Gram GLOBAL: ssrbinder; ssrbinder: [ - [ ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" -> { + [ ["of" -> { () } | "&" -> { () } ]; c = term LEVEL "99" -> { (FwdPose, [BFvar]), CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Glob_term.Explicit,c)],mkCHole (Some loc)) } ] ]; @@ -1594,18 +1594,18 @@ GRAMMAR EXTEND Gram | n = Prim.natural -> { ArgArg (check_index ~loc n) } ] ]; ssrswap: [[ IDENT "first" -> { loc, true } | IDENT "last" -> { loc, false } ]]; - ssrorelse: [[ "||"; tac = tactic_expr LEVEL "2" -> { tac } ]]; + ssrorelse: [[ "||"; tac = ltac_expr LEVEL "2" -> { tac } ]]; ssrseqarg: [ [ arg = ssrswap -> { noindex, swaptacarg arg } | i = ssrseqidx; tac = ssrortacarg; def = OPT ssrorelse -> { i, (tac, def) } | i = ssrseqidx; arg = ssrswap -> { i, swaptacarg arg } - | tac = tactic_expr LEVEL "3" -> { noindex, (mk_hint tac, None) } + | tac = ltac_expr LEVEL "3" -> { noindex, (mk_hint tac, None) } ] ]; END { -let tactic_expr = Pltac.tactic_expr +let ltac_expr = Pltac.ltac_expr } @@ -1688,9 +1688,9 @@ let tclintros_expr ?loc tac ipats = } GRAMMAR EXTEND Gram - GLOBAL: tactic_expr; - tactic_expr: LEVEL "1" [ RIGHTA - [ tac = tactic_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros } + GLOBAL: ltac_expr; + ltac_expr: LEVEL "1" [ RIGHTA + [ tac = ltac_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros } ] ]; END @@ -1704,9 +1704,9 @@ END (* (Removing user-specified parentheses is dubious anyway). *) GRAMMAR EXTEND Gram - GLOBAL: tactic_expr; - ssrparentacarg: [[ "("; tac = tactic_expr; ")" -> { CAst.make ~loc (Tacexp tac) } ]]; - tactic_expr: LEVEL "0" [[ arg = ssrparentacarg -> { TacArg arg } ]]; + GLOBAL: ltac_expr; + ssrparentacarg: [[ "("; tac = ltac_expr; ")" -> { CAst.make ~loc (Tacexp tac) } ]]; + ltac_expr: LEVEL "0" [[ arg = ssrparentacarg -> { TacArg arg } ]]; END (** The internal "done" and "ssrautoprop" tactics. *) @@ -1741,7 +1741,7 @@ let tclBY tac = Tacticals.New.tclTHEN tac (donetac ~-1) (* The latter two are used in forward-chaining tactics (have, suffice, wlog) *) (* and subgoal reordering tacticals (; first & ; last), respectively. *) -(* Force use of the tactic_expr parsing entry, to rule out tick marks. *) +(* Force use of the ltac_expr parsing entry, to rule out tick marks. *) (** The "by" tactical. *) @@ -1782,12 +1782,12 @@ let ssrdotac_expr ?loc n m tac clauses = } GRAMMAR EXTEND Gram - GLOBAL: tactic_expr; + GLOBAL: ltac_expr; ssrdotac: [ - [ tac = tactic_expr LEVEL "3" -> { mk_hint tac } + [ tac = ltac_expr LEVEL "3" -> { mk_hint tac } | tacs = ssrortacarg -> { tacs } ] ]; - tactic_expr: LEVEL "3" [ RIGHTA + ltac_expr: LEVEL "3" [ RIGHTA [ IDENT "do"; m = ssrmmod; tac = ssrdotac; clauses = ssrclauses -> { ssrdotac_expr ~loc noindex m tac clauses } | IDENT "do"; tac = ssrortacarg; clauses = ssrclauses -> @@ -1833,20 +1833,20 @@ let tclseq_expr ?loc tac dir arg = } GRAMMAR EXTEND Gram - GLOBAL: tactic_expr; + GLOBAL: ltac_expr; ssr_first: [ [ tac = ssr_first; ipats = ssrintros_ne -> { tclintros_expr ~loc tac ipats } - | "["; tacl = LIST0 tactic_expr SEP "|"; "]" -> { TacFirst tacl } + | "["; tacl = LIST0 ltac_expr SEP "|"; "]" -> { TacFirst tacl } ] ]; ssr_first_else: [ [ tac1 = ssr_first; tac2 = ssrorelse -> { TacOrelse (tac1, tac2) } | tac = ssr_first -> { tac } ]]; - tactic_expr: LEVEL "4" [ LEFTA - [ tac1 = tactic_expr; ";"; IDENT "first"; tac2 = ssr_first_else -> + ltac_expr: LEVEL "4" [ LEFTA + [ tac1 = ltac_expr; ";"; IDENT "first"; tac2 = ssr_first_else -> { TacThen (tac1, tac2) } - | tac = tactic_expr; ";"; IDENT "first"; arg = ssrseqarg -> + | tac = ltac_expr; ";"; IDENT "first"; arg = ssrseqarg -> { tclseq_expr ~loc tac L2R arg } - | tac = tactic_expr; ";"; IDENT "last"; arg = ssrseqarg -> + | tac = ltac_expr; ";"; IDENT "last"; arg = ssrseqarg -> { tclseq_expr ~loc tac R2L arg } ] ]; END @@ -2447,8 +2447,8 @@ END (* The standard TACTIC EXTEND does not work for abstract *) GRAMMAR EXTEND Gram - GLOBAL: tactic_expr; - tactic_expr: LEVEL "3" + GLOBAL: ltac_expr; + ltac_expr: LEVEL "3" [ RIGHTA [ IDENT "abstract"; gens = ssrdgens -> { ssrtac_expr ~loc "abstract" [Tacexpr.TacGeneric (None, Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)] } ]]; diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 91cd5b251c..a49a5e8b28 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -85,7 +85,7 @@ let mk_pat c (na, t) = (c, na, t) GRAMMAR EXTEND Gram GLOBAL: binder_constr; - ssr_rtype: [[ "return"; t = operconstr LEVEL "100" -> { mk_rtype t } ]]; + ssr_rtype: [[ "return"; t = term LEVEL "100" -> { mk_rtype t } ]]; ssr_mpat: [[ p = pattern -> { [[p]] } ]]; ssr_dpat: [ [ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> { mp, mk_ctype mp t, rt } @@ -96,9 +96,9 @@ GRAMMAR EXTEND Gram ssr_elsepat: [[ "else" -> { [[CAst.make ~loc @@ CPatAtom None]] } ]]; ssr_else: [[ mp = ssr_elsepat; c = lconstr -> { CAst.make ~loc (mp, c) } ]]; binder_constr: [ - [ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else -> + [ "if"; c = term LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else -> { let b1, ct, rt = db1 in CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) } - | "if"; c = operconstr LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else -> + | "if"; c = term LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else -> { let b1, ct, rt = db1 in let b1, b2 = let open CAst in let {loc=l1; v=(p1, r1)}, {loc=l2; v=(p2, r2)} = b1, b2 in @@ -119,7 +119,7 @@ END GRAMMAR EXTEND Gram GLOBAL: closed_binder; closed_binder: [ - [ ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" -> + [ ["of" -> { () } | "&" -> { () } ]; c = term LEVEL "99" -> { [CLocalAssum ([CAst.make ~loc Anonymous], Default Explicit, c)] } ] ]; END diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index c030925ea9..93d91abea3 100644 --- a/plugins/syntax/g_numeral.mlg +++ b/plugins/syntax/g_numeral.mlg @@ -31,7 +31,7 @@ let warn_deprecated_numeral_notation = } -VERNAC ARGUMENT EXTEND numnotoption +VERNAC ARGUMENT EXTEND numeral_modifier PRINTED BY { pr_numnot_option } | [ ] -> { Nop } | [ "(" "warning" "after" bignat(waft) ")" ] -> { Warning (NumTok.UnsignedNat.of_string waft) } @@ -40,11 +40,11 @@ END VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF | #[ locality = Attributes.locality; ] [ "Number" "Notation" reference(ty) reference(f) reference(g) ":" - ident(sc) numnotoption(o) ] -> + ident(sc) numeral_modifier(o) ] -> { vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" - ident(sc) numnotoption(o) ] -> + ident(sc) numeral_modifier(o) ] -> { warn_deprecated_numeral_notation (); vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } diff --git a/test-suite/misc/quotation_token/src/quotation.mlg b/test-suite/misc/quotation_token/src/quotation.mlg index 961b170a0d..ba0bcb1b3c 100644 --- a/test-suite/misc/quotation_token/src/quotation.mlg +++ b/test-suite/misc/quotation_token/src/quotation.mlg @@ -2,9 +2,9 @@ open Pcoq.Constr } GRAMMAR EXTEND Gram - GLOBAL: operconstr; + GLOBAL: term; - operconstr: LEVEL "0" + term: LEVEL "0" [ [ s = QUOTATION "foobar:" -> { CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [GProp,0])) } ] ] diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index a42518822f..fa0c20bf73 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -8,7 +8,7 @@ Entry custom:myconstr is | "4" RIGHTA [ SELF; "*"; NEXT ] | "3" RIGHTA - [ "<"; operconstr LEVEL "10"; ">" ] ] + [ "<"; term LEVEL "10"; ">" ] ] [< b > + < b > * < 2 >] : nat @@ -77,7 +77,7 @@ The command has indeed failed with message: The format is not the same on the right- and left-hand sides of the special token "..". Entry custom:expr is [ "201" RIGHTA - [ "{"; operconstr LEVEL "200"; "}" ] ] + [ "{"; term LEVEL "200"; "}" ] ] fun x : nat => [ x ] : nat -> nat diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index cecc6c66d2..6749169e8c 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -71,8 +71,9 @@ let test_ltac1_env = lk_ident_list >> lk_kw "|-" end -let tac2expr = Tac2entries.Pltac.tac2expr -let tac2type = Entry.create "tac2type" +let ltac2_expr = Tac2entries.Pltac.ltac2_expr +let _ltac2_expr = ltac2_expr +let ltac2_type = Entry.create "ltac2_type" let tac2def_val = Entry.create "tac2def_val" let tac2def_typ = Entry.create "tac2def_typ" let tac2def_ext = Entry.create "tac2def_ext" @@ -80,7 +81,7 @@ let tac2def_syn = Entry.create "tac2def_syn" let tac2def_mut = Entry.create "tac2def_mut" let tac2mode = Entry.create "ltac2_command" -let ltac1_expr = Pltac.tactic_expr +let ltac_expr = Pltac.ltac_expr let tac2expr_in_env = Tac2entries.Pltac.tac2expr_in_env let inj_wit wit loc x = CAst.make ~loc @@ CTacExt (wit, x) @@ -101,7 +102,7 @@ let pattern_of_qualid qid = } GRAMMAR EXTEND Gram - GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext tac2def_syn + GLOBAL: ltac2_expr ltac2_type tac2def_val tac2def_typ tac2def_ext tac2def_syn tac2def_mut tac2expr_in_env; tac2pat: [ "1" LEFTA @@ -125,7 +126,7 @@ GRAMMAR EXTEND Gram atomic_tac2pat: [ [ -> { CAst.make ~loc @@ CPatRef (AbsKn (Tuple 0), []) } - | p = tac2pat; ":"; t = tac2type -> + | p = tac2pat; ":"; t = ltac2_type -> { CAst.make ~loc @@ CPatCnv (p, t) } | p = tac2pat; ","; pl = LIST0 tac2pat SEP "," -> { let pl = p :: pl in @@ -133,17 +134,17 @@ GRAMMAR EXTEND Gram | p = tac2pat -> { p } ] ] ; - tac2expr: + ltac2_expr: [ "6" RIGHTA [ e1 = SELF; ";"; e2 = SELF -> { CAst.make ~loc @@ CTacSeq (e1, e2) } ] | "5" - [ "fun"; it = LIST1 input_fun ; "=>"; body = tac2expr LEVEL "6" -> + [ "fun"; it = LIST1 input_fun ; "=>"; body = ltac2_expr LEVEL "6" -> { CAst.make ~loc @@ CTacFun (it, body) } | "let"; isrec = rec_flag; lc = LIST1 let_clause SEP "with"; "in"; - e = tac2expr LEVEL "6" -> + e = ltac2_expr LEVEL "6" -> { CAst.make ~loc @@ CTacLet (isrec, lc, e) } - | "match"; e = tac2expr LEVEL "5"; "with"; bl = branches; "end" -> + | "match"; e = ltac2_expr LEVEL "5"; "with"; bl = branches; "end" -> { CAst.make ~loc @@ CTacCse (e, bl) } ] | "4" LEFTA [ ] @@ -151,25 +152,25 @@ GRAMMAR EXTEND Gram { let el = e0 :: el in CAst.make ~loc @@ CTacApp (CAst.make ~loc @@ CTacCst (AbsKn (Tuple (List.length el))), el) } ] | "2" RIGHTA - [ e1 = tac2expr; "::"; e2 = tac2expr -> + [ e1 = ltac2_expr; "::"; e2 = ltac2_expr -> { CAst.make ~loc @@ CTacApp (CAst.make ~loc @@ CTacCst (AbsKn (Other Tac2core.Core.c_cons)), [e1; e2]) } ] | "1" LEFTA - [ e = tac2expr; el = LIST1 tac2expr LEVEL "0" -> + [ e = ltac2_expr; el = LIST1 ltac2_expr LEVEL "0" -> { CAst.make ~loc @@ CTacApp (e, el) } | e = SELF; ".("; qid = Prim.qualid; ")" -> { CAst.make ~loc @@ CTacPrj (e, RelId qid) } - | e = SELF; ".("; qid = Prim.qualid; ")"; ":="; r = tac2expr LEVEL "5" -> + | e = SELF; ".("; qid = Prim.qualid; ")"; ":="; r = ltac2_expr LEVEL "5" -> { CAst.make ~loc @@ CTacSet (e, RelId qid, r) } ] | "0" [ "("; a = SELF; ")" -> { a } - | "("; a = SELF; ":"; t = tac2type; ")" -> + | "("; a = SELF; ":"; t = ltac2_type; ")" -> { CAst.make ~loc @@ CTacCnv (a, t) } | "()" -> { CAst.make ~loc @@ CTacCst (AbsKn (Tuple 0)) } | "("; ")" -> { CAst.make ~loc @@ CTacCst (AbsKn (Tuple 0)) } - | "["; a = LIST0 tac2expr LEVEL "5" SEP ";"; "]" -> + | "["; a = LIST0 ltac2_expr LEVEL "5" SEP ";"; "]" -> { Tac2quote.of_list ~loc (fun x -> x) a } | "{"; a = tac2rec_fieldexprs; "}" -> { CAst.make ~loc @@ CTacRec a } @@ -183,7 +184,7 @@ GRAMMAR EXTEND Gram ] ; branch: - [ [ pat = tac2pat LEVEL "1"; "=>"; e = tac2expr LEVEL "6" -> { (pat, e) } ] ] + [ [ pat = tac2pat LEVEL "1"; "=>"; e = ltac2_expr LEVEL "6" -> { (pat, e) } ] ] ; rec_flag: [ [ IDENT "rec" -> { true } @@ -193,7 +194,7 @@ GRAMMAR EXTEND Gram [ [ IDENT "mutable" -> { true } | -> { false } ] ] ; - typ_param: + ltac2_typevar: [ [ "'"; id = Prim.ident -> { id } ] ] ; tactic_atom: @@ -210,19 +211,19 @@ GRAMMAR EXTEND Gram | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> { Tac2quote.of_constr c } | IDENT "open_constr"; ":"; "("; c = Constr.lconstr; ")" -> { Tac2quote.of_open_constr c } | IDENT "ident"; ":"; "("; c = lident; ")" -> { Tac2quote.of_ident c } - | IDENT "pattern"; ":"; "("; c = Constr.lconstr_pattern; ")" -> { inj_pattern loc c } + | IDENT "pattern"; ":"; "("; c = Constr.cpattern; ")" -> { inj_pattern loc c } | IDENT "reference"; ":"; "("; c = globref; ")" -> { inj_reference loc c } | IDENT "ltac1"; ":"; "("; qid = ltac1_expr_in_env; ")" -> { inj_ltac1 loc qid } | IDENT "ltac1val"; ":"; "("; qid = ltac1_expr_in_env; ")" -> { inj_ltac1val loc qid } ] ] ; ltac1_expr_in_env: - [ [ test_ltac1_env; ids = LIST0 locident; "|-"; e = ltac1_expr -> { ids, e } - | e = ltac1_expr -> { [], e } + [ [ test_ltac1_env; ids = LIST0 locident; "|-"; e = ltac_expr -> { ids, e } + | e = ltac_expr -> { [], e } ] ] ; tac2expr_in_env : - [ [ test_ltac1_env; ids = LIST0 locident; "|-"; e = tac2expr -> + [ [ test_ltac1_env; ids = LIST0 locident; "|-"; e = ltac2_expr -> { let check { CAst.v = id; CAst.loc = loc } = if Tac2env.is_constructor (Libnames.qualid_of_ident ?loc id) then CErrors.user_err ?loc Pp.(str "Invalid bound Ltac2 identifier " ++ Id.print id) @@ -230,11 +231,11 @@ GRAMMAR EXTEND Gram let () = List.iter check ids in (ids, e) } - | tac = tac2expr -> { [], tac } + | tac = ltac2_expr -> { [], tac } ] ] ; let_clause: - [ [ binder = let_binder; ":="; te = tac2expr -> + [ [ binder = let_binder; ":="; te = ltac2_expr -> { let (pat, fn) = binder in let te = match fn with | None -> te @@ -252,23 +253,23 @@ GRAMMAR EXTEND Gram | _ -> CErrors.user_err ~loc (str "Invalid pattern") } ] ] ; - tac2type: + ltac2_type: [ "5" RIGHTA - [ t1 = tac2type; "->"; t2 = tac2type -> { CAst.make ~loc @@ CTypArrow (t1, t2) } ] + [ t1 = ltac2_type; "->"; t2 = ltac2_type -> { CAst.make ~loc @@ CTypArrow (t1, t2) } ] | "2" - [ t = tac2type; "*"; tl = LIST1 tac2type LEVEL "1" SEP "*" -> + [ t = ltac2_type; "*"; tl = LIST1 ltac2_type LEVEL "1" SEP "*" -> { let tl = t :: tl in CAst.make ~loc @@ CTypRef (AbsKn (Tuple (List.length tl)), tl) } ] | "1" LEFTA [ t = SELF; qid = Prim.qualid -> { CAst.make ~loc @@ CTypRef (RelId qid, [t]) } ] | "0" - [ "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = OPT Prim.qualid -> + [ "("; p = LIST1 ltac2_type LEVEL "5" SEP ","; ")"; qid = OPT Prim.qualid -> { match p, qid with | [t], None -> t | _, None -> CErrors.user_err ~loc (Pp.str "Syntax error") | ts, Some qid -> CAst.make ~loc @@ CTypRef (RelId qid, p) } - | id = typ_param -> { CAst.make ~loc @@ CTypVar (Name id) } + | id = ltac2_typevar -> { CAst.make ~loc @@ CTypVar (Name id) } | "_" -> { CAst.make ~loc @@ CTypVar Anonymous } | qid = Prim.qualid -> { CAst.make ~loc @@ CTypRef (RelId qid, []) } ] @@ -284,7 +285,7 @@ GRAMMAR EXTEND Gram [ [ b = tac2pat LEVEL "0" -> { b } ] ] ; tac2def_body: - [ [ name = binder; it = LIST0 input_fun; ":="; e = tac2expr -> + [ [ name = binder; it = LIST0 input_fun; ":="; e = ltac2_expr -> { let e = if List.is_empty it then e else CAst.make ~loc @@ CTacFun (it, e) in (name, e) } ] ] @@ -295,10 +296,10 @@ GRAMMAR EXTEND Gram ] ] ; tac2def_mut: - [ [ "Set"; qid = Prim.qualid; old = OPT [ "as"; id = locident -> { id } ]; ":="; e = tac2expr -> { StrMut (qid, old, e) } ] ] + [ [ "Set"; qid = Prim.qualid; old = OPT [ "as"; id = locident -> { id } ]; ":="; e = ltac2_expr -> { StrMut (qid, old, e) } ] ] ; tac2typ_knd: - [ [ t = tac2type -> { CTydDef (Some t) } + [ [ t = ltac2_type -> { CTydDef (Some t) } | "["; ".."; "]" -> { CTydOpn } | "["; t = tac2alg_constructors; "]" -> { CTydAlg t } | "{"; t = tac2rec_fields; "}"-> { CTydRec t } ] ] @@ -309,7 +310,7 @@ GRAMMAR EXTEND Gram ; tac2alg_constructor: [ [ c = Prim.ident -> { (c, []) } - | c = Prim.ident; "("; args = LIST0 tac2type SEP ","; ")"-> { (c, args) } ] ] + | c = Prim.ident; "("; args = LIST0 ltac2_type SEP ","; ")"-> { (c, args) } ] ] ; tac2rec_fields: [ [ f = tac2rec_field; ";"; l = tac2rec_fields -> { f :: l } @@ -318,7 +319,7 @@ GRAMMAR EXTEND Gram | -> { [] } ] ] ; tac2rec_field: - [ [ mut = mut_flag; id = Prim.ident; ":"; t = tac2type -> { (id, mut, t) } ] ] + [ [ mut = mut_flag; id = Prim.ident; ":"; t = ltac2_type -> { (id, mut, t) } ] ] ; tac2rec_fieldexprs: [ [ f = tac2rec_fieldexpr; ";"; l = tac2rec_fieldexprs -> { f :: l } @@ -327,12 +328,12 @@ GRAMMAR EXTEND Gram | -> { [] } ] ] ; tac2rec_fieldexpr: - [ [ qid = Prim.qualid; ":="; e = tac2expr LEVEL "1" -> { RelId qid, e } ] ] + [ [ qid = Prim.qualid; ":="; e = ltac2_expr LEVEL "1" -> { RelId qid, e } ] ] ; tac2typ_prm: [ [ -> { [] } - | id = typ_param -> { [CAst.make ~loc id] } - | "("; ids = LIST1 [ id = typ_param -> { CAst.make ~loc id } ] SEP "," ;")" -> { ids } + | id = ltac2_typevar -> { [CAst.make ~loc id] } + | "("; ids = LIST1 [ id = ltac2_typevar -> { CAst.make ~loc id } ] SEP "," ;")" -> { ids } ] ] ; tac2typ_def: @@ -350,7 +351,7 @@ GRAMMAR EXTEND Gram ] ] ; tac2def_ext: - [ [ "@"; IDENT "external"; id = locident; ":"; t = tac2type LEVEL "5"; ":="; + [ [ "@"; IDENT "external"; id = locident; ":"; t = ltac2_type LEVEL "5"; ":="; plugin = Prim.string; name = Prim.string -> { let ml = { mltac_plugin = plugin; mltac_tactic = name } in StrPrm (id, t, ml) } @@ -361,11 +362,11 @@ GRAMMAR EXTEND Gram | id = Prim.ident -> { CAst.make ~loc (Some id) } ] ] ; - sexpr: + ltac2_scope: [ [ s = Prim.string -> { SexprStr (CAst.make ~loc s) } | n = Prim.integer -> { SexprInt (CAst.make ~loc n) } | id = syn_node -> { SexprRec (loc, id, []) } - | id = syn_node; "("; tok = LIST1 sexpr SEP "," ; ")" -> + | id = syn_node; "("; tok = LIST1 ltac2_scope SEP "," ; ")" -> { SexprRec (loc, id, tok) } ] ] ; @@ -375,8 +376,8 @@ GRAMMAR EXTEND Gram ] ] ; tac2def_syn: - [ [ "Notation"; toks = LIST1 sexpr; n = syn_level; ":="; - e = tac2expr -> + [ [ "Notation"; toks = LIST1 ltac2_scope; n = syn_level; ":="; + e = ltac2_expr -> { StrSyn (toks, n, e) } ] ] ; @@ -497,7 +498,7 @@ GRAMMAR EXTEND Gram ; simple_intropattern: [ [ pat = simple_intropattern_closed -> -(* l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] -> *) +(* l = LIST0 ["%"; c = term LEVEL "0" -> c] -> *) (** TODO: handle %pat *) { pat } ] ] @@ -654,26 +655,26 @@ GRAMMAR EXTEND Gram [ [ r = oriented_rewriter -> { r } ] ] ; tactic_then_last: - [ [ "|"; lta = LIST0 (OPT tac2expr LEVEL "6") SEP "|" -> { lta } + [ [ "|"; lta = LIST0 (OPT ltac2_expr LEVEL "6") SEP "|" -> { lta } | -> { [] } ] ] ; - tactic_then_gen: - [ [ ta = tac2expr; "|"; tg = tactic_then_gen -> { let (first,last) = tg in (Some ta :: first, last) } - | ta = tac2expr; ".."; l = tactic_then_last -> { ([], Some (Some ta, l)) } + for_each_goal: + [ [ ta = ltac2_expr; "|"; tg = for_each_goal -> { let (first,last) = tg in (Some ta :: first, last) } + | ta = ltac2_expr; ".."; l = tactic_then_last -> { ([], Some (Some ta, l)) } | ".."; l = tactic_then_last -> { ([], Some (None, l)) } - | ta = tac2expr -> { ([Some ta], None) } - | "|"; tg = tactic_then_gen -> { let (first,last) = tg in (None :: first, last) } + | ta = ltac2_expr -> { ([Some ta], None) } + | "|"; tg = for_each_goal -> { let (first,last) = tg in (None :: first, last) } | -> { ([None], None) } ] ] ; q_dispatch: - [ [ d = tactic_then_gen -> { CAst.make ~loc d } ] ] + [ [ d = for_each_goal -> { CAst.make ~loc d } ] ] ; q_occurrences: [ [ occs = occs -> { occs } ] ] ; - red_flag: + ltac2_red_flag: [ [ IDENT "beta" -> { CAst.make ~loc @@ QBeta } | IDENT "iota" -> { CAst.make ~loc @@ QIota } | IDENT "match" -> { CAst.make ~loc @@ QMatch } @@ -702,7 +703,7 @@ GRAMMAR EXTEND Gram ] ] ; strategy_flag: - [ [ s = LIST1 red_flag -> { CAst.make ~loc s } + [ [ s = LIST1 ltac2_red_flag -> { CAst.make ~loc s } | d = delta_flag -> { CAst.make ~loc [CAst.make ~loc QBeta; CAst.make ~loc QIota; CAst.make ~loc QZeta; d] } @@ -721,11 +722,11 @@ GRAMMAR EXTEND Gram ; match_pattern: [ [ IDENT "context"; id = OPT Prim.ident; - "["; pat = Constr.lconstr_pattern; "]" -> { CAst.make ~loc @@ QConstrMatchContext (id, pat) } - | pat = Constr.lconstr_pattern -> { CAst.make ~loc @@ QConstrMatchPattern pat } ] ] + "["; pat = Constr.cpattern; "]" -> { CAst.make ~loc @@ QConstrMatchContext (id, pat) } + | pat = Constr.cpattern -> { CAst.make ~loc @@ QConstrMatchPattern pat } ] ] ; match_rule: - [ [ mp = match_pattern; "=>"; tac = tac2expr -> + [ [ mp = match_pattern; "=>"; tac = ltac2_expr -> { CAst.make ~loc @@ (mp, tac) } ] ] ; @@ -748,16 +749,16 @@ GRAMMAR EXTEND Gram ] ] ; gmatch_rule: - [ [ mp = gmatch_pattern; "=>"; tac = tac2expr -> + [ [ mp = gmatch_pattern; "=>"; tac = ltac2_expr -> { CAst.make ~loc @@ (mp, tac) } ] ] ; - gmatch_list: + goal_match_list: [ [ mrl = LIST1 gmatch_rule SEP "|" -> { CAst.make ~loc @@ mrl } | "|"; mrl = LIST1 gmatch_rule SEP "|" -> { CAst.make ~loc @@ mrl } ] ] ; q_goal_matching: - [ [ m = gmatch_list -> { m } ] ] + [ [ m = goal_match_list -> { m } ] ] ; move_location: [ [ "at"; IDENT "top" -> { CAst.make ~loc @@ QMoveFirst } @@ -789,7 +790,7 @@ GRAMMAR EXTEND Gram ] ] ; by_tactic: - [ [ "by"; tac = tac2expr -> { Some tac } + [ [ "by"; tac = ltac2_expr -> { Some tac } | -> { None } ] ] ; @@ -812,8 +813,8 @@ END (* GRAMMAR EXTEND Gram - Pcoq.Constr.operconstr: LEVEL "0" - [ [ IDENT "ltac2"; ":"; "("; tac = tac2expr; ")" -> + Pcoq.Constr.term: LEVEL "0" + [ [ IDENT "ltac2"; ":"; "("; tac = ltac2_expr; ")" -> { let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg)) } | test_ampersand_ident; "&"; id = Prim.ident -> @@ -858,7 +859,7 @@ let rules = [ Pcoq.( Production.make (Rule.stop ++ Symbol.token (PIDENT (Some "ltac2")) ++ Symbol.token (PKEYWORD ":") ++ - Symbol.token (PKEYWORD "(") ++ Symbol.nterm tac2expr ++ Symbol.token (PKEYWORD ")")) + Symbol.token (PKEYWORD "(") ++ Symbol.nterm ltac2_expr ++ Symbol.token (PKEYWORD ")")) begin fun _ tac _ _ _ loc -> let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg)) @@ -867,7 +868,7 @@ let rules = [ ] in Hook.set Tac2entries.register_constr_quotations begin fun () -> - Pcoq.grammar_extend Pcoq.Constr.operconstr {pos=Some (Gramlib.Gramext.Level "0"); data=[(None, None, rules)]} + Pcoq.grammar_extend Pcoq.Constr.term {pos=Some (Gramlib.Gramext.Level "0"); data=[(None, None, rules)]} end } @@ -890,7 +891,7 @@ END VERNAC ARGUMENT EXTEND ltac2_expr PRINTED BY { pr_ltac2expr } -| [ tac2expr(e) ] -> { e } +| [ _ltac2_expr(e) ] -> { e } END { diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 3ce50865c0..5d49d1635c 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1541,12 +1541,12 @@ end let () = add_scope "tactic" begin function | [] -> (* Default to level 5 parsing *) - let scope = Pcoq.Symbol.nterml tac2expr "5" in + let scope = Pcoq.Symbol.nterml ltac2_expr "5" in let act tac = tac in Tac2entries.ScopeRule (scope, act) | [SexprInt {loc;v=n}] as arg -> let () = if n < 0 || n > 6 then scope_fail "tactic" arg in - let scope = Pcoq.Symbol.nterml tac2expr (string_of_int n) in + let scope = Pcoq.Symbol.nterml ltac2_expr (string_of_int n) in let act tac = tac in Tac2entries.ScopeRule (scope, act) | arg -> scope_fail "tactic" arg diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index 03789fff6c..eebd6635fa 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -24,7 +24,8 @@ open Tac2intern module Pltac = struct -let tac2expr = Pcoq.Entry.create "tac2expr" +let ltac2_expr = Pcoq.Entry.create "ltac2_expr" +let tac2expr = ltac2_expr let tac2expr_in_env = Pcoq.Entry.create "tac2expr_in_env" let q_ident = Pcoq.Entry.create "q_ident" @@ -643,7 +644,7 @@ let perform_notation syn st = | Some lev -> Some (string_of_int lev) in let rule = (lev, None, [rule]) in - ([Pcoq.ExtendRule (Pltac.tac2expr, {Pcoq.pos=None; data=[rule]})], st) + ([Pcoq.ExtendRule (Pltac.ltac2_expr, {Pcoq.pos=None; data=[rule]})], st) let ltac2_notation = Pcoq.create_grammar_command "ltac2-notation" perform_notation diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli index 2f053df2d0..782968c6e1 100644 --- a/user-contrib/Ltac2/tac2entries.mli +++ b/user-contrib/Ltac2/tac2entries.mli @@ -63,7 +63,9 @@ val backtrace : backtrace Exninfo.t module Pltac : sig +val ltac2_expr : raw_tacexpr Pcoq.Entry.t val tac2expr : raw_tacexpr Pcoq.Entry.t + [@@deprecated "Deprecated in 8.13; use 'ltac2_expr' instead"] val tac2expr_in_env : (Id.t CAst.t list * raw_tacexpr) Pcoq.Entry.t (** Quoted entries. To be used for complex notations. *) diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index b134f7b82b..123ea2c24e 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -300,13 +300,13 @@ let interp_constr_entry_key : type r. _ -> r target -> int -> r Entry.t * int op match forpat with | ForConstr -> if level = 200 then Constr.binder_constr, None - else Constr.operconstr, Some level + else Constr.term, Some level | ForPattern -> Constr.pattern, Some level let target_entry : type s. notation_entry -> s target -> s Entry.t = function | InConstrEntry -> (function - | ForConstr -> Constr.operconstr + | ForConstr -> Constr.term | ForPattern -> Constr.pattern) | InCustomEntry s -> let (entry_for_constr, entry_for_patttern) = find_custom_entry s in diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index dfc7b05b51..3d6a93c888 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -48,7 +48,7 @@ let assumption_token = Entry.create "assumption_token" let def_body = Entry.create "def_body" let decl_notations = Entry.create "decl_notations" let record_field = Entry.create "record_field" -let of_type_with_opt_coercion = Entry.create "of_type_with_opt_coercion" +let of_type = Entry.create "of_type" let section_subset_expr = Entry.create "section_subset_expr" let scope_delimiter = Entry.create "scope_delimiter" let syntax_modifiers = Entry.create "syntax_modifiers" @@ -113,10 +113,10 @@ GRAMMAR EXTEND Gram ] ; attribute: - [ [ k = ident ; v = attribute_value -> { Names.Id.to_string k, v } ] + [ [ k = ident ; v = attr_value -> { Names.Id.to_string k, v } ] ] ; - attribute_value: + attr_value: [ [ "=" ; v = string -> { VernacFlagLeaf v } | "(" ; a = attribute_list ; ")" -> { VernacFlagList a } | -> { VernacFlagEmpty } ] @@ -196,8 +196,8 @@ let name_of_ident_decl : ident_decl -> name_decl = (* Gallina declarations *) GRAMMAR EXTEND Gram - GLOBAL: gallina gallina_ext thm_token def_token assumption_token def_body of_type_with_opt_coercion - record_field decl_notations rec_definition ident_decl univ_decl; + GLOBAL: gallina gallina_ext thm_token def_token assumption_token def_body of_type + record_field decl_notations fix_definition ident_decl univ_decl; gallina: (* Definition, Theorem, Variable, Axiom, ... *) @@ -219,13 +219,13 @@ GRAMMAR EXTEND Gram (* Gallina inductive declarations *) | f = finite_token; indl = LIST1 inductive_definition SEP "with" -> { VernacInductive (f, indl) } - | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> + | "Fixpoint"; recs = LIST1 fix_definition SEP "with" -> { VernacFixpoint (NoDischarge, recs) } - | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> + | IDENT "Let"; "Fixpoint"; recs = LIST1 fix_definition SEP "with" -> { VernacFixpoint (DoDischarge, recs) } - | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> + | "CoFixpoint"; corecs = LIST1 cofix_definition SEP "with" -> { VernacCoFixpoint (NoDischarge, corecs) } - | IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> + | IDENT "Let"; "CoFixpoint"; corecs = LIST1 cofix_definition SEP "with" -> { VernacCoFixpoint (DoDischarge, corecs) } | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> { VernacScheme l } | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; @@ -339,7 +339,7 @@ GRAMMAR EXTEND Gram ; (* Inductives and records *) opt_constructors_or_fields: - [ [ ":="; lc = constructor_list_or_record_decl -> { lc } + [ [ ":="; lc = constructors_or_record -> { lc } | -> { RecordDecl (None, []) } ] ] ; inductive_definition: @@ -349,7 +349,7 @@ GRAMMAR EXTEND Gram lc=opt_constructors_or_fields; ntn = decl_notations -> { (((oc,id),(indpar,extrapar),c,lc),ntn) } ] ] ; - constructor_list_or_record_decl: + constructors_or_record: [ [ "|"; l = LIST1 constructor SEP "|" -> { Constructors l } | id = identref ; c = constructor_type; "|"; l = LIST1 constructor SEP "|" -> { Constructors ((c id)::l) } @@ -369,7 +369,7 @@ GRAMMAR EXTEND Gram | -> { false } ] ] ; (* (co)-fixpoints *) - rec_definition: + fix_definition: [ [ id_decl = ident_decl; bl = binders_fixannot; rtype = type_cstr; @@ -378,7 +378,7 @@ GRAMMAR EXTEND Gram {fname = fst id_decl; univs = snd id_decl; rec_order; binders; rtype; body_def; notations} } ] ] ; - corec_definition: + cofix_definition: [ [ id_decl = ident_decl; binders = binders; rtype = type_cstr; body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notations -> { {fname = fst id_decl; univs = snd id_decl; rec_order = (); binders; rtype; body_def; notations} @@ -427,10 +427,10 @@ GRAMMAR EXTEND Gram | -> { [] } ] ] ; - record_binder_body: - [ [ l = binders; oc = of_type_with_opt_coercion; + field_body: + [ [ l = binders; oc = of_type; t = lconstr -> { fun id -> (oc,AssumExpr (id,l,t)) } - | l = binders; oc = of_type_with_opt_coercion; + | l = binders; oc = of_type; t = lconstr; ":="; b = lconstr -> { fun id -> (oc,DefExpr (id,l,b,Some t)) } | l = binders; ":="; b = lconstr -> { fun id -> @@ -442,22 +442,22 @@ GRAMMAR EXTEND Gram ; record_binder: [ [ id = name -> { (NoInstance,AssumExpr(id, [], CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) } - | id = name; f = record_binder_body -> { f id } ] ] + | id = name; f = field_body -> { f id } ] ] ; assum_list: - [ [ bl = LIST1 assum_coe -> { bl } | b = simple_assum_coe -> { [b] } ] ] + [ [ bl = LIST1 assum_coe -> { bl } | b = assumpt -> { [b] } ] ] ; assum_coe: - [ [ "("; a = simple_assum_coe; ")" -> { a } ] ] + [ [ "("; a = assumpt; ")" -> { a } ] ] ; - simple_assum_coe: - [ [ idl = LIST1 ident_decl; oc = of_type_with_opt_coercion; c = lconstr -> + assumpt: + [ [ idl = LIST1 ident_decl; oc = of_type; c = lconstr -> { (oc <> NoInstance,(idl,c)) } ] ] ; constructor_type: [[ l = binders; - t= [ coe = of_type_with_opt_coercion; c = lconstr -> + t= [ coe = of_type; c = lconstr -> { fun l id -> (coe <> NoInstance,(id,mkProdCN ~loc l c)) } | -> { fun l id -> (false,(id,mkProdCN ~loc l (CAst.make ~loc @@ CHole (None, IntroAnonymous, None)))) } ] @@ -468,7 +468,7 @@ GRAMMAR EXTEND Gram constructor: [ [ id = identref; c=constructor_type -> { c id } ] ] ; - of_type_with_opt_coercion: + of_type: [ [ ":>" -> { BackInstance } | ":"; ">" -> { BackInstance } | ":" -> { NoInstance } ] ] @@ -687,7 +687,7 @@ GRAMMAR EXTEND Gram { VernacContext (List.flatten c) } | IDENT "Instance"; namesup = instance_name; ":"; - t = operconstr LEVEL "200"; + t = term LEVEL "200"; info = hint_info ; props = [ ":="; "{"; r = record_declaration; "}" -> { Some (true,r) } | ":="; c = lconstr -> { Some (false,c) } | -> { None } ] -> @@ -707,13 +707,13 @@ GRAMMAR EXTEND Gram (* Arguments *) | IDENT "Arguments"; qid = smart_global; - args = LIST0 argument_spec_block; + args = LIST0 arg_specs; more_implicits = OPT [ ","; impl = LIST1 - [ impl = LIST0 more_implicits_block -> { List.flatten impl } ] + [ impl = LIST0 implicits_alt -> { List.flatten impl } ] SEP "," -> { impl } ]; - mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> { l } ] -> + mods = OPT [ ":"; l = LIST1 args_modifier SEP "," -> { l } ] -> { let mods = match mods with None -> [] | Some l -> List.flatten l in let more_implicits = Option.default [] more_implicits in VernacArguments (qid, List.flatten args, more_implicits, mods) } @@ -732,7 +732,7 @@ GRAMMAR EXTEND Gram idl = LIST1 identref -> { Some idl } ] -> { VernacGeneralizable gen } ] ] ; - arguments_modifier: + args_modifier: [ [ IDENT "simpl"; IDENT "nomatch" -> { [`ReductionDontExposeCase] } | IDENT "simpl"; IDENT "never" -> { [`ReductionNeverUnfold] } | IDENT "default"; IDENT "implicits" -> { [`DefaultImplicits] } @@ -757,7 +757,7 @@ GRAMMAR EXTEND Gram ] ]; (* List of arguments implicit status, scope, modifiers *) - argument_spec_block: [ + arg_specs: [ [ item = argument_spec -> { let name, recarg_like, notation_scope = item in [RealArg { name=name; recarg_like=recarg_like; @@ -791,8 +791,8 @@ GRAMMAR EXTEND Gram implicit_status = MaxImplicit}) items } ] ]; - (* Same as [argument_spec_block], but with only implicit status and names *) - more_implicits_block: [ + (* Same as [arg_specs], but with only implicit status and names *) + implicits_alt: [ [ name = name -> { [(name.CAst.v, Explicit)] } | "["; items = LIST1 name; "]" -> { List.map (fun name -> (name.CAst.v, NonMaxImplicit)) items } @@ -826,9 +826,9 @@ GRAMMAR EXTEND Gram GLOBAL: command query_command class_rawexpr gallina_ext search_query search_queries; gallina_ext: - [ [ IDENT "Export"; "Set"; table = option_table; v = option_setting -> + [ [ IDENT "Export"; "Set"; table = setting_name; v = option_setting -> { VernacSetOption (true, table, v) } - | IDENT "Export"; IDENT "Unset"; table = option_table -> + | IDENT "Export"; IDENT "Unset"; table = setting_name -> { VernacSetOption (true, table, OptionUnset) } ] ]; @@ -837,7 +837,7 @@ GRAMMAR EXTEND Gram (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *) | IDENT "Declare"; IDENT "Instance"; id = ident_decl; bl = binders; ":"; - t = operconstr LEVEL "200"; + t = term LEVEL "200"; info = hint_info -> { VernacDeclareInstance (id, bl, t, info) } @@ -885,12 +885,12 @@ GRAMMAR EXTEND Gram { VernacAddMLPath dir } (* For acting on parameter tables *) - | "Set"; table = option_table; v = option_setting -> + | "Set"; table = setting_name; v = option_setting -> { VernacSetOption (false, table, v) } - | IDENT "Unset"; table = option_table -> + | IDENT "Unset"; table = setting_name -> { VernacSetOption (false, table, OptionUnset) } - | IDENT "Print"; IDENT "Table"; table = option_table -> + | IDENT "Print"; IDENT "Table"; table = setting_name -> { VernacPrintOption table } | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 table_value @@ -902,9 +902,9 @@ GRAMMAR EXTEND Gram | IDENT "Add"; table = IDENT; v = LIST1 table_value -> { VernacAddOption ([table], v) } - | IDENT "Test"; table = option_table; "for"; v = LIST1 table_value + | IDENT "Test"; table = setting_name; "for"; v = LIST1 table_value -> { VernacMemOption (table, v) } - | IDENT "Test"; table = option_table -> + | IDENT "Test"; table = setting_name -> { VernacPrintOption table } | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 table_value @@ -1006,7 +1006,7 @@ GRAMMAR EXTEND Gram [ [ id = global -> { Goptions.QualidRefValue id } | s = STRING -> { Goptions.StringRefValue s } ] ] ; - option_table: + setting_name: [ [ fl = LIST1 [ x = IDENT -> { x } ] -> { fl } ]] ; ne_in_or_out_modules: @@ -1191,10 +1191,10 @@ GRAMMAR EXTEND Gram | s, None -> SetFormat ("text",s) end } | x = IDENT; ","; l = LIST1 [id = IDENT -> { id } ] SEP ","; "at"; lev = level -> { SetItemLevel (x::l,None,lev) } - | x = IDENT; "at"; lev = level; b = OPT constr_as_binder_kind -> + | x = IDENT; "at"; lev = level; b = OPT binder_interp -> { SetItemLevel ([x],b,lev) } - | x = IDENT; b = constr_as_binder_kind -> { SetItemLevel ([x],Some b,DefaultLevel) } - | x = IDENT; typ = syntax_extension_type -> { SetEntryType (x,typ) } + | x = IDENT; b = binder_interp -> { SetItemLevel ([x],Some b,DefaultLevel) } + | x = IDENT; typ = explicit_subentry -> { SetEntryType (x,typ) } ] ] ; syntax_modifiers: @@ -1202,18 +1202,18 @@ GRAMMAR EXTEND Gram | -> { [] } ] ] ; - syntax_extension_type: + explicit_subentry: [ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal } | IDENT "bigint" -> { ETBigint } | IDENT "binder" -> { ETBinder true } | IDENT "constr" -> { ETConstr (InConstrEntry,None,DefaultLevel) } - | IDENT "constr"; n = at_level_opt; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) } + | IDENT "constr"; n = at_level_opt; b = OPT binder_interp -> { ETConstr (InConstrEntry,b,n) } | IDENT "pattern" -> { ETPattern (false,None) } | IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (false,Some n) } | IDENT "strict"; IDENT "pattern" -> { ETPattern (true,None) } | IDENT "strict"; IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (true,Some n) } | IDENT "closed"; IDENT "binder" -> { ETBinder false } - | IDENT "custom"; x = IDENT; n = at_level_opt; b = OPT constr_as_binder_kind -> + | IDENT "custom"; x = IDENT; n = at_level_opt; b = OPT binder_interp -> { ETConstr (InCustomEntry x,b,n) } ] ] ; @@ -1221,7 +1221,7 @@ GRAMMAR EXTEND Gram [ [ "at"; n = level -> { n } | -> { DefaultLevel } ] ] ; - constr_as_binder_kind: + binder_interp: [ [ "as"; IDENT "ident" -> { Notation_term.AsIdent } | "as"; IDENT "pattern" -> { Notation_term.AsIdentOrPattern } | "as"; IDENT "strict"; IDENT "pattern" -> { Notation_term.AsStrictPattern } ] ] diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 8ce59c40c3..185abcf35b 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -61,15 +61,15 @@ let pr_registered_grammar name = prlist pr_one entries let pr_grammar = function - | "constr" | "operconstr" | "binder_constr" -> + | "constr" | "term" | "binder_constr" -> str "Entry constr is" ++ fnl () ++ pr_entry Pcoq.Constr.constr ++ str "and lconstr is" ++ fnl () ++ pr_entry Pcoq.Constr.lconstr ++ str "where binder_constr is" ++ fnl () ++ pr_entry Pcoq.Constr.binder_constr ++ - str "and operconstr is" ++ fnl () ++ - pr_entry Pcoq.Constr.operconstr + str "and term is" ++ fnl () ++ + pr_entry Pcoq.Constr.term | "pattern" -> pr_entry Pcoq.Constr.pattern | "vernac" -> diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index c9f68eed57..a7de34dd09 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -43,7 +43,8 @@ module Vernac_ = let command = Entry.create "command" let syntax = Entry.create "syntax_command" let vernac_control = Entry.create "Vernac.vernac_control" - let rec_definition = Entry.create "Vernac.rec_definition" + let fix_definition = Entry.create "Vernac.fix_definition" + let rec_definition = fix_definition let red_expr = Entry.create "red_expr" let hint_info = Entry.create "hint_info" (* Main vernac entry *) diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli index 8ab4af7d48..dac6877cb3 100644 --- a/vernac/pvernac.mli +++ b/vernac/pvernac.mli @@ -25,7 +25,9 @@ module Vernac_ : val command : vernac_expr Entry.t val syntax : vernac_expr Entry.t val vernac_control : vernac_control Entry.t + val fix_definition : fixpoint_expr Entry.t val rec_definition : fixpoint_expr Entry.t + [@@deprecated "Deprecated in 8.13; use 'fix_definition' instead"] val noedit_mode : vernac_expr Entry.t val command_entry : vernac_expr Entry.t val main_entry : vernac_control option Entry.t |