diff options
| author | Pierre-Marie Pédrot | 2021-03-10 12:17:32 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-10 12:20:27 +0100 |
| commit | aba594ca194390bb00f8ef60ef8a5eef6694fc07 (patch) | |
| tree | 2106e5937035b46bb8cea34a127e6903c0151561 /doc/sphinx | |
| parent | 14d391651041291995c435cc8669e0f4a3146abb (diff) | |
Regenerate the Ltac2 syntax for documentation.
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 6 |
1 files changed, 3 insertions, 3 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 |