Regenerate the Ltac2 syntax for documentation.

4 files changed, 501 insertions, 495 deletions

diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 9f3f0ef3d5..146da8bb37 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -263,10 +263,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 +304,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
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: [