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/tools/docgram/orderedGrammar | 1 +
 1 file changed, 1 insertion(+)

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

diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 12a7bc684d..7d773e3a5b 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1640,6 +1640,7 @@ simple_tactic: [
 | "ring" OPT ( "[" LIST1 one_term "]" )
 | "ring_simplify" OPT ( "[" LIST1 one_term "]" ) LIST1 one_term OPT ( "in" ident )
 | "match" ltac2_expr5 "with" OPT ltac2_branches "end"
+| "if" ltac2_expr5 "then" ltac2_expr5 "else" ltac2_expr5
 | qualid LIST1 tactic_arg
 ]
 
-- 
cgit v1.2.3