From aba594ca194390bb00f8ef60ef8a5eef6694fc07 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 10 Mar 2021 12:17:32 +0100
Subject: Regenerate the Ltac2 syntax for documentation.

---
 doc/sphinx/proof-engine/ltac2.rst | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc/sphinx')

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
-- 
cgit v1.2.3