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/tools/docgram/orderedGrammar | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc/tools/docgram/orderedGrammar')

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