From 1b0e754ccf22cc1a7ae50a7b1d8350197ec2981b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 2 Nov 2020 13:45:08 +0100
Subject: Regenerate the grammar description file.

---
 doc/sphinx/proof-engine/ltac2.rst | 1 -
 1 file changed, 1 deletion(-)

(limited to 'doc/sphinx')

diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index d4e49dda5b..41f376c43d 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -266,7 +266,6 @@ There is dedicated syntax for list and array literals.
    | @ltac2_expr5
    ltac2_expr5 ::= fun {+ @tac2pat0 } => @ltac2_expr
    | let {? rec } @ltac2_let_clause {* with @ltac2_let_clause } in @ltac2_expr
-   | if @ltac2_expr5 then @ltac2_expr5 else @ltac2_expr5
    | @ltac2_expr3
    ltac2_let_clause ::= {+ @tac2pat0 } := @ltac2_expr
    ltac2_expr3 ::= {+, @ltac2_expr2 }
-- 
cgit v1.2.3