diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/05-tactic-language/13774-ltac2-deprecated-attribute-term.rst | 6 | ||||
| -rw-r--r-- | doc/changelog/05-tactic-language/13914-ltac2-cast-fun-return.rst | 5 | ||||
| -rw-r--r-- | doc/changelog/10-standard-library/13582-exp_ineq.rst | 4 | ||||
| -rw-r--r-- | doc/changelog/10-standard-library/13671-Vector_to_list.rst | 4 | ||||
| -rw-r--r-- | doc/changelog/10-standard-library/13804-count_occ.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 15 | ||||
| -rw-r--r-- | doc/sphinx/using/libraries/writing.rst | 6 | ||||
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 1 | ||||
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 983 | ||||
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 6 |
10 files changed, 534 insertions, 500 deletions
diff --git a/doc/changelog/05-tactic-language/13774-ltac2-deprecated-attribute-term.rst b/doc/changelog/05-tactic-language/13774-ltac2-deprecated-attribute-term.rst new file mode 100644 index 0000000000..5fdfbd9796 --- /dev/null +++ b/doc/changelog/05-tactic-language/13774-ltac2-deprecated-attribute-term.rst @@ -0,0 +1,6 @@ +- **Added:** + Ltac2 commands defining terms now accept the :attr:`deprecated` + attribute + (`#13774 <https://github.com/coq/coq/pull/13774>`_, + fixes `#12317 <https://github.com/coq/coq/issues/12317>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/05-tactic-language/13914-ltac2-cast-fun-return.rst b/doc/changelog/05-tactic-language/13914-ltac2-cast-fun-return.rst new file mode 100644 index 0000000000..5ecc5934eb --- /dev/null +++ b/doc/changelog/05-tactic-language/13914-ltac2-cast-fun-return.rst @@ -0,0 +1,5 @@ +- **Added:** + Allow the presence of type casts for function return values, let bindings and + global definitions in Ltac2 + (`#13914 <https://github.com/coq/coq/pull/13914>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/10-standard-library/13582-exp_ineq.rst b/doc/changelog/10-standard-library/13582-exp_ineq.rst index 27d89b2f8b..ff4e8db8b0 100644 --- a/doc/changelog/10-standard-library/13582-exp_ineq.rst +++ b/doc/changelog/10-standard-library/13582-exp_ineq.rst @@ -4,6 +4,4 @@ Adds exp_ineq1_le, which holds for all reals (but is a <= instead of a <). (`#13582 <https://github.com/coq/coq/pull/13582>`_, - by Avi Shinnar and Barry Trager, with help from Laurent Théry - -). + by Avi Shinnar and Barry Trager, with help from Laurent Théry). diff --git a/doc/changelog/10-standard-library/13671-Vector_to_list.rst b/doc/changelog/10-standard-library/13671-Vector_to_list.rst new file mode 100644 index 0000000000..e8404f0c93 --- /dev/null +++ b/doc/changelog/10-standard-library/13671-Vector_to_list.rst @@ -0,0 +1,4 @@ +- **Added:** + Lemmas about vectors related with ``to_list``: ``length_to_list``, ``of_list_to_list_opp``, ``to_list_nil``, ``to_list_cons``, ``to_list_hd``, ``to_list_last``, ``to_list_const``, ``to_list_nth_order``, ``to_list_tl``, ``to_list_append``, ``to_list_rev_append_tail``, ``to_list_rev_append``, ``to_list_rev``, ``to_list_map``, ``to_list_fold_left``, ``to_list_fold_right``, ``to_list_Forall``, ``to_list_Exists``, ``to_list_In``, ``to_list_Forall2`` + (`#13671 <https://github.com/coq/coq/pull/13671>`_, + by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/13804-count_occ.rst b/doc/changelog/10-standard-library/13804-count_occ.rst new file mode 100644 index 0000000000..9354b219d8 --- /dev/null +++ b/doc/changelog/10-standard-library/13804-count_occ.rst @@ -0,0 +1,4 @@ +- **Added:** + Lemmas about ``count_occ``: ``count_occ_app``, ``count_occ_elt_eq``, ``count_occ_elt_neq``, ``count_occ_bound``, ``count_occ_repeat_eq``, ``count_occ_repeat_neq``, ``count_occ_unique``, ``count_occ_repeat_excl``, ``count_occ_sgt``, ``Permutation_count_occ`` + (`#13804 <https://github.com/coq/coq/pull/13804>`_, + by Olivier Laurent with help of Jean-Christophe Léchenet). diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 9f3f0ef3d5..294c56ef06 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -66,7 +66,6 @@ Current limitations include: - An easy way to get the number of constructors of an inductive type. Currently only way to do this is to destruct a variable of the inductive type and count the number of goals that result. -- The :attr:`deprecated` attribute is not supported for Ltac2 definitions. - Error messages may be cryptic. @@ -229,6 +228,8 @@ One can define new types with the following commands. defined in Coq and give their type information. They can also declare data structures from OCaml. This command has no use for the end user. + This command supports the :attr:`deprecated` attribute. + APIs ~~~~ @@ -263,10 +264,10 @@ There is dedicated syntax for list and array literals. .. prodn:: ltac2_expr ::= @ltac2_expr5 ; @ltac2_expr | @ltac2_expr5 - ltac2_expr5 ::= fun {+ @tac2pat0 } => @ltac2_expr + ltac2_expr5 ::= fun {+ @tac2pat0 } {? : @ltac2_type } => @ltac2_expr | let {? rec } @ltac2_let_clause {* with @ltac2_let_clause } in @ltac2_expr | @ltac2_expr3 - ltac2_let_clause ::= {+ @tac2pat0 } := @ltac2_expr + ltac2_let_clause ::= {+ @tac2pat0 } {? : @ltac2_type } := @ltac2_expr ltac2_expr3 ::= {+, @ltac2_expr2 } ltac2_expr2 ::= @ltac2_expr1 :: @ltac2_expr2 | @ltac2_expr1 @@ -304,7 +305,7 @@ Ltac2 Definitions .. insertprodn tac2def_body tac2def_body .. prodn:: - tac2def_body ::= {| _ | @ident } {* @tac2pat0 } := @ltac2_expr + tac2def_body ::= {| _ | @ident } {* @tac2pat0 } {? : @ltac2_type } := @ltac2_expr This command defines a new global Ltac2 value. If one or more :token:`tac2pat0` are specified, the new value is a function. This is a shortcut for one of the @@ -319,6 +320,8 @@ Ltac2 Definitions If ``mutable`` is set, the definition can be redefined at a later stage (see below). + This command supports the :attr:`deprecated` attribute. + .. cmd:: Ltac2 Set @qualid {? as @ident } := @ltac2_expr This command redefines a previous ``mutable`` definition. @@ -1246,6 +1249,8 @@ Notations so that you may have to resort to thunking to ensure that side-effects are performed at the right time. + This command supports the :attr:`deprecated` attribute. + Abbreviations ~~~~~~~~~~~~~ @@ -1276,6 +1281,8 @@ Abbreviations Note that abbreviations are not type checked at all, and may result in typing errors after expansion. + This command supports the :attr:`deprecated` attribute. + .. _defining_tactics: Defining tactics diff --git a/doc/sphinx/using/libraries/writing.rst b/doc/sphinx/using/libraries/writing.rst index 917edf0774..7461bfe443 100644 --- a/doc/sphinx/using/libraries/writing.rst +++ b/doc/sphinx/using/libraries/writing.rst @@ -22,13 +22,17 @@ deprecated compatibility alias using :cmd:`Notation (abbreviation)` by a comma. This attribute is supported by the following commands: :cmd:`Ltac`, - :cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`. + :cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`, :cmd:`Ltac2`, + :cmd:`Ltac2 Notation`, :cmd:`Ltac2 external`. It can trigger the following warnings: .. warn:: Tactic @qualid is deprecated since @string__since. @string__note. Tactic Notation @qualid is deprecated since @string__since. @string__note. Notation @string is deprecated since @string__since. @string__note. + Ltac2 definition @qualid is deprecated since @string__since. @string__note. + Ltac2 alias @qualid is deprecated since @string__since. @string__note. + Ltac2 notation {+ @ltac2_scope } is deprecated since @string__since. @string__note. :n:`@qualid` or :n:`@string` is the notation, :n:`@string__since` is the version number, :n:`@string__note` is diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 24ecc65e9b..fd1c3c0260 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -2730,6 +2730,7 @@ SPLICE: [ | variance_identref | rewriter | conversion +| type_cast ] (* end SPLICE *) RENAME: [ diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index be1b9d80fb..ab1a9d4c75 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1,6 +1,492 @@ (* Coq grammar generated from .mlg files. Do not edit by hand. Not compiled into Coq *) DOC_GRAMMAR +Constr.ident: [ +| Prim.ident +] + +Prim.name: [ +| "_" +] + +global: [ +| Prim.reference +] + +constr_pattern: [ +| constr +] + +cpattern: [ +| lconstr +] + +sort: [ +| "Set" +| "Prop" +| "SProp" +| "Type" +| "Type" "@{" "_" "}" +| "Type" "@{" universe "}" +] + +sort_family: [ +| "Set" +| "Prop" +| "SProp" +| "Type" +] + +universe_increment: [ +| "+" natural +| +] + +universe_name: [ +| global +| "Set" +| "Prop" +] + +universe_expr: [ +| universe_name universe_increment +] + +universe: [ +| "max" "(" LIST1 universe_expr SEP "," ")" +| universe_expr +] + +lconstr: [ +| term200 +] + +constr: [ +| term8 +| "@" global univ_annot +] + +term200: [ +| binder_constr +| term100 +] + +term100: [ +| term99 "<:" term200 +| term99 "<<:" term200 +| term99 ":" term200 +| term99 ":>" +| term99 +] + +term99: [ +| term90 +] + +term90: [ +| term10 +] + +term10: [ +| term9 LIST1 arg +| "@" global univ_annot LIST0 term9 +| "@" pattern_ident LIST1 identref +| term9 +] + +term9: [ +| ".." term0 ".." +| term8 +] + +term8: [ +| term1 +] + +term1: [ +| term0 ".(" global LIST0 arg ")" +| term0 ".(" "@" global LIST0 ( term9 ) ")" +| term0 "%" IDENT +| term0 +] + +term0: [ +| atomic_constr +| term_match +| "(" term200 ")" +| "{|" record_declaration bar_cbrace +| "{" binder_constr "}" +| "`{" term200 "}" +| test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_annot +| "`(" term200 ")" +| "ltac" ":" "(" Pltac.ltac_expr ")" +] + +array_elems: [ +| LIST0 lconstr SEP ";" +] + +record_declaration: [ +| fields_def +] + +fields_def: [ +| field_def ";" fields_def +| field_def +| +] + +field_def: [ +| global binders ":=" lconstr +] + +binder_constr: [ +| "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 +| "if" term200 "is" ssr_dthen ssr_else (* SSR plugin *) +| "if" term200 "isn't" ssr_dthen ssr_else (* SSR plugin *) +| "let" ":" ssr_mpat ":=" lconstr "in" lconstr (* SSR plugin *) +| "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr (* SSR plugin *) +| "let" ":" ssr_mpat "in" pattern200 ":=" lconstr ssr_rtype "in" lconstr (* SSR plugin *) +] + +arg: [ +| test_lpar_id_coloneq "(" identref ":=" lconstr ")" +| term9 +] + +atomic_constr: [ +| global univ_annot +| sort +| NUMBER +| string +| "_" +| "?" "[" identref "]" +| "?" "[" pattern_ident "]" +| pattern_ident evar_instance +] + +inst: [ +| identref ":=" lconstr +] + +evar_instance: [ +| "@{" LIST1 inst SEP ";" "}" +| +] + +univ_annot: [ +| "@{" LIST0 universe_level "}" +| +] + +universe_level: [ +| "Set" +| "Prop" +| "Type" +| "_" +| global +] + +fix_decls: [ +| fix_decl +| fix_decl "with" LIST1 fix_decl SEP "with" "for" identref +] + +cofix_decls: [ +| cofix_body +| cofix_body "with" LIST1 cofix_body SEP "with" "for" identref +] + +fix_decl: [ +| identref binders_fixannot type_cstr ":=" term200 +] + +cofix_body: [ +| identref binders type_cstr ":=" term200 +] + +term_match: [ +| "match" LIST1 case_item SEP "," OPT case_type "with" branches "end" +] + +case_item: [ +| term100 OPT [ "as" name ] OPT [ "in" pattern200 ] +] + +case_type: [ +| "return" term100 +] + +as_return_type: [ +| OPT [ OPT [ "as" name ] case_type ] +] + +branches: [ +| OPT "|" LIST0 eqn SEP "|" +] + +mult_pattern: [ +| LIST1 pattern200 SEP "," +] + +eqn: [ +| LIST1 mult_pattern SEP "|" "=>" lconstr +] + +record_pattern: [ +| global ":=" pattern200 +] + +record_patterns: [ +| record_pattern ";" record_patterns +| record_pattern +| +] + +pattern200: [ +| pattern100 +] + +pattern100: [ +| pattern99 ":" term200 +| pattern99 +] + +pattern99: [ +| pattern90 +] + +pattern90: [ +| pattern10 +] + +pattern10: [ +| pattern1 "as" name +| pattern1 LIST1 pattern1 +| "@" Prim.reference LIST0 pattern1 +| pattern1 +] + +pattern1: [ +| pattern0 "%" IDENT +| pattern0 +] + +pattern0: [ +| Prim.reference +| "{|" record_patterns bar_cbrace +| "_" +| "(" pattern200 ")" +| "(" pattern200 "|" LIST1 pattern200 SEP "|" ")" +| NUMBER +| string +] + +fixannot: [ +| "{" "struct" identref "}" +| "{" "wf" constr identref "}" +| "{" "measure" constr OPT identref OPT constr "}" +] + +binders_fixannot: [ +| ensure_fixannot fixannot +| binder binders_fixannot +| +] + +open_binders: [ +| name LIST0 name ":" lconstr +| name LIST0 name binders +| name ".." name +| closed_binder binders +] + +binders: [ +| LIST0 binder +| Pcoq.Constr.binders +] + +binder: [ +| name +| closed_binder +] + +closed_binder: [ +| "(" name LIST1 name ":" lconstr ")" +| "(" name ":" lconstr ")" +| "(" name ":=" lconstr ")" +| "(" name ":" lconstr ":=" lconstr ")" +| "{" name "}" +| "{" name LIST1 name ":" lconstr "}" +| "{" name ":" lconstr "}" +| "{" name LIST1 name "}" +| "[" name "]" +| "[" name LIST1 name ":" lconstr "]" +| "[" name ":" lconstr "]" +| "[" name LIST1 name "]" +| "`(" LIST1 typeclass_constraint SEP "," ")" +| "`{" LIST1 typeclass_constraint SEP "," "}" +| "`[" LIST1 typeclass_constraint SEP "," "]" +| "'" pattern0 +| [ "of" | "&" ] term99 (* SSR plugin *) +] + +one_open_binder: [ +| name +| name ":" lconstr +| one_closed_binder +] + +one_closed_binder: [ +| "(" name ":" lconstr ")" +| "{" name "}" +| "{" name ":" lconstr "}" +| "[" name "]" +| "[" name ":" lconstr "]" +| "'" pattern0 +] + +typeclass_constraint: [ +| "!" term200 +| "{" name "}" ":" [ "!" | ] term200 +| test_name_colon name ":" [ "!" | ] term200 +| term200 +] + +type_cstr: [ +| ":" lconstr +| +] + +let_type_cstr: [ +| OPT [ ":" lconstr ] +] + +preident: [ +| IDENT +] + +ident: [ +| IDENT +] + +pattern_ident: [ +| LEFTQMARK ident +] + +identref: [ +| ident +] + +hyp: [ +| identref +] + +field: [ +| FIELD +] + +fields: [ +| field fields +| field +] + +fullyqualid: [ +| ident fields +| ident +] + +name: [ +| "_" +| ident +] + +reference: [ +| ident fields +| ident +] + +qualid: [ +| reference +] + +by_notation: [ +| ne_string OPT [ "%" IDENT ] +] + +smart_global: [ +| reference +| by_notation +] + +ne_string: [ +| STRING +] + +ne_lstring: [ +| ne_string +] + +dirpath: [ +| ident LIST0 field +] + +string: [ +| STRING +] + +lstring: [ +| string +] + +integer: [ +| bigint +] + +natural: [ +| bignat +] + +bigint: [ +| bignat +| test_minus_nat "-" bignat +] + +bignat: [ +| NUMBER +] + +bar_cbrace: [ +| test_pipe_closedcurly "|" "}" +] + +strategy_level: [ +| "expand" +| "opaque" +| integer +| "transparent" +] + +vernac_toplevel: [ +| "Drop" "." +| "Quit" "." +| "BackTo" natural "." +| test_show_goal "Show" "Goal" natural "at" natural "." +| "Show" "Proof" "Diffs" OPT "removed" "." +| Pvernac.Vernac_.main_entry +] + opt_hintbases: [ | | ":" LIST1 IDENT @@ -981,492 +1467,6 @@ binder_interp: [ | "as" "strict" "pattern" ] -vernac_toplevel: [ -| "Drop" "." -| "Quit" "." -| "BackTo" natural "." -| test_show_goal "Show" "Goal" natural "at" natural "." -| "Show" "Proof" "Diffs" OPT "removed" "." -| Pvernac.Vernac_.main_entry -] - -Constr.ident: [ -| Prim.ident -] - -Prim.name: [ -| "_" -] - -global: [ -| Prim.reference -] - -constr_pattern: [ -| constr -] - -cpattern: [ -| lconstr -] - -sort: [ -| "Set" -| "Prop" -| "SProp" -| "Type" -| "Type" "@{" "_" "}" -| "Type" "@{" universe "}" -] - -sort_family: [ -| "Set" -| "Prop" -| "SProp" -| "Type" -] - -universe_increment: [ -| "+" natural -| -] - -universe_name: [ -| global -| "Set" -| "Prop" -] - -universe_expr: [ -| universe_name universe_increment -] - -universe: [ -| "max" "(" LIST1 universe_expr SEP "," ")" -| universe_expr -] - -lconstr: [ -| term200 -] - -constr: [ -| term8 -| "@" global univ_annot -] - -term200: [ -| binder_constr -| term100 -] - -term100: [ -| term99 "<:" term200 -| term99 "<<:" term200 -| term99 ":" term200 -| term99 ":>" -| term99 -] - -term99: [ -| term90 -] - -term90: [ -| term10 -] - -term10: [ -| term9 LIST1 arg -| "@" global univ_annot LIST0 term9 -| "@" pattern_ident LIST1 identref -| term9 -] - -term9: [ -| ".." term0 ".." -| term8 -] - -term8: [ -| term1 -] - -term1: [ -| term0 ".(" global LIST0 arg ")" -| term0 ".(" "@" global LIST0 ( term9 ) ")" -| term0 "%" IDENT -| term0 -] - -term0: [ -| atomic_constr -| term_match -| "(" term200 ")" -| "{|" record_declaration bar_cbrace -| "{" binder_constr "}" -| "`{" term200 "}" -| test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_annot -| "`(" term200 ")" -| "ltac" ":" "(" Pltac.ltac_expr ")" -] - -array_elems: [ -| LIST0 lconstr SEP ";" -] - -record_declaration: [ -| fields_def -] - -fields_def: [ -| field_def ";" fields_def -| field_def -| -] - -field_def: [ -| global binders ":=" lconstr -] - -binder_constr: [ -| "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 -| "if" term200 "is" ssr_dthen ssr_else (* SSR plugin *) -| "if" term200 "isn't" ssr_dthen ssr_else (* SSR plugin *) -| "let" ":" ssr_mpat ":=" lconstr "in" lconstr (* SSR plugin *) -| "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr (* SSR plugin *) -| "let" ":" ssr_mpat "in" pattern200 ":=" lconstr ssr_rtype "in" lconstr (* SSR plugin *) -] - -arg: [ -| test_lpar_id_coloneq "(" identref ":=" lconstr ")" -| term9 -] - -atomic_constr: [ -| global univ_annot -| sort -| NUMBER -| string -| "_" -| "?" "[" identref "]" -| "?" "[" pattern_ident "]" -| pattern_ident evar_instance -] - -inst: [ -| identref ":=" lconstr -] - -evar_instance: [ -| "@{" LIST1 inst SEP ";" "}" -| -] - -univ_annot: [ -| "@{" LIST0 universe_level "}" -| -] - -universe_level: [ -| "Set" -| "Prop" -| "Type" -| "_" -| global -] - -fix_decls: [ -| fix_decl -| fix_decl "with" LIST1 fix_decl SEP "with" "for" identref -] - -cofix_decls: [ -| cofix_body -| cofix_body "with" LIST1 cofix_body SEP "with" "for" identref -] - -fix_decl: [ -| identref binders_fixannot type_cstr ":=" term200 -] - -cofix_body: [ -| identref binders type_cstr ":=" term200 -] - -term_match: [ -| "match" LIST1 case_item SEP "," OPT case_type "with" branches "end" -] - -case_item: [ -| term100 OPT [ "as" name ] OPT [ "in" pattern200 ] -] - -case_type: [ -| "return" term100 -] - -as_return_type: [ -| OPT [ OPT [ "as" name ] case_type ] -] - -branches: [ -| OPT "|" LIST0 eqn SEP "|" -] - -mult_pattern: [ -| LIST1 pattern200 SEP "," -] - -eqn: [ -| LIST1 mult_pattern SEP "|" "=>" lconstr -] - -record_pattern: [ -| global ":=" pattern200 -] - -record_patterns: [ -| record_pattern ";" record_patterns -| record_pattern -| -] - -pattern200: [ -| pattern100 -] - -pattern100: [ -| pattern99 ":" term200 -| pattern99 -] - -pattern99: [ -| pattern90 -] - -pattern90: [ -| pattern10 -] - -pattern10: [ -| pattern1 "as" name -| pattern1 LIST1 pattern1 -| "@" Prim.reference LIST0 pattern1 -| pattern1 -] - -pattern1: [ -| pattern0 "%" IDENT -| pattern0 -] - -pattern0: [ -| Prim.reference -| "{|" record_patterns bar_cbrace -| "_" -| "(" pattern200 ")" -| "(" pattern200 "|" LIST1 pattern200 SEP "|" ")" -| NUMBER -| string -] - -fixannot: [ -| "{" "struct" identref "}" -| "{" "wf" constr identref "}" -| "{" "measure" constr OPT identref OPT constr "}" -] - -binders_fixannot: [ -| ensure_fixannot fixannot -| binder binders_fixannot -| -] - -open_binders: [ -| name LIST0 name ":" lconstr -| name LIST0 name binders -| name ".." name -| closed_binder binders -] - -binders: [ -| LIST0 binder -| Pcoq.Constr.binders -] - -binder: [ -| name -| closed_binder -] - -closed_binder: [ -| "(" name LIST1 name ":" lconstr ")" -| "(" name ":" lconstr ")" -| "(" name ":=" lconstr ")" -| "(" name ":" lconstr ":=" lconstr ")" -| "{" name "}" -| "{" name LIST1 name ":" lconstr "}" -| "{" name ":" lconstr "}" -| "{" name LIST1 name "}" -| "[" name "]" -| "[" name LIST1 name ":" lconstr "]" -| "[" name ":" lconstr "]" -| "[" name LIST1 name "]" -| "`(" LIST1 typeclass_constraint SEP "," ")" -| "`{" LIST1 typeclass_constraint SEP "," "}" -| "`[" LIST1 typeclass_constraint SEP "," "]" -| "'" pattern0 -| [ "of" | "&" ] term99 (* SSR plugin *) -] - -one_open_binder: [ -| name -| name ":" lconstr -| one_closed_binder -] - -one_closed_binder: [ -| "(" name ":" lconstr ")" -| "{" name "}" -| "{" name ":" lconstr "}" -| "[" name "]" -| "[" name ":" lconstr "]" -| "'" pattern0 -] - -typeclass_constraint: [ -| "!" term200 -| "{" name "}" ":" [ "!" | ] term200 -| test_name_colon name ":" [ "!" | ] term200 -| term200 -] - -type_cstr: [ -| ":" lconstr -| -] - -let_type_cstr: [ -| OPT [ ":" lconstr ] -] - -preident: [ -| IDENT -] - -ident: [ -| IDENT -] - -pattern_ident: [ -| LEFTQMARK ident -] - -identref: [ -| ident -] - -hyp: [ -| identref -] - -field: [ -| FIELD -] - -fields: [ -| field fields -| field -] - -fullyqualid: [ -| ident fields -| ident -] - -name: [ -| "_" -| ident -] - -reference: [ -| ident fields -| ident -] - -qualid: [ -| reference -] - -by_notation: [ -| ne_string OPT [ "%" IDENT ] -] - -smart_global: [ -| reference -| by_notation -] - -ne_string: [ -| STRING -] - -ne_lstring: [ -| ne_string -] - -dirpath: [ -| ident LIST0 field -] - -string: [ -| STRING -] - -lstring: [ -| string -] - -integer: [ -| bigint -] - -natural: [ -| bignat -] - -bigint: [ -| bignat -| test_minus_nat "-" bignat -] - -bignat: [ -| NUMBER -] - -bar_cbrace: [ -| test_pipe_closedcurly "|" "}" -] - -strategy_level: [ -| "expand" -| "opaque" -| integer -| "transparent" -] - simple_tactic: [ | "btauto" | "congruence" @@ -3283,7 +3283,7 @@ ltac2_expr6: [ ] ltac2_expr5: [ -| "fun" LIST1 G_LTAC2_input_fun "=>" ltac2_expr6 (* Ltac2 plugin *) +| "fun" LIST1 G_LTAC2_input_fun type_cast "=>" 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 *) | "if" ltac2_expr5 "then" ltac2_expr5 "else" ltac2_expr5 (* Ltac2 plugin *) @@ -3371,8 +3371,13 @@ tac2expr_in_env: [ | ltac2_expr6 (* Ltac2 plugin *) ] +type_cast: [ +| (* Ltac2 plugin *) +| ":" ltac2_type5 (* Ltac2 plugin *) +] + G_LTAC2_let_clause: [ -| let_binder ":=" ltac2_expr6 (* Ltac2 plugin *) +| let_binder type_cast ":=" ltac2_expr6 (* Ltac2 plugin *) ] let_binder: [ @@ -3415,7 +3420,7 @@ G_LTAC2_input_fun: [ ] tac2def_body: [ -| G_LTAC2_binder LIST0 G_LTAC2_input_fun ":=" ltac2_expr6 (* Ltac2 plugin *) +| G_LTAC2_binder LIST0 G_LTAC2_input_fun type_cast ":=" ltac2_expr6 (* Ltac2 plugin *) ] tac2def_val: [ diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 5674d28139..5b19b7fc55 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -2274,7 +2274,7 @@ ltac2_entry: [ ] tac2def_body: [ -| [ "_" | ident ] LIST0 tac2pat0 ":=" ltac2_expr (* Ltac2 plugin *) +| [ "_" | ident ] LIST0 tac2pat0 OPT ( ":" ltac2_type ) ":=" ltac2_expr (* Ltac2 plugin *) ] tac2typ_def: [ @@ -2315,13 +2315,13 @@ ltac2_expr: [ ] ltac2_expr5: [ -| "fun" LIST1 tac2pat0 "=>" ltac2_expr (* Ltac2 plugin *) +| "fun" LIST1 tac2pat0 OPT ( ":" ltac2_type ) "=>" ltac2_expr (* Ltac2 plugin *) | "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" ltac2_expr (* Ltac2 plugin *) | ltac2_expr3 (* Ltac2 plugin *) ] ltac2_let_clause: [ -| LIST1 tac2pat0 ":=" ltac2_expr (* Ltac2 plugin *) +| LIST1 tac2pat0 OPT ( ":" ltac2_type ) ":=" ltac2_expr (* Ltac2 plugin *) ] ltac2_expr3: [ |