diff options
| author | Pierre-Marie Pédrot | 2020-11-02 13:45:08 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-04 17:53:02 +0100 |
| commit | 1b0e754ccf22cc1a7ae50a7b1d8350197ec2981b (patch) | |
| tree | 5acc63968c526ec7b4825c342f434acc0e5c01d9 | |
| parent | 2559f0474c8cd66b5020524d1e758ea7a19bc8fb (diff) | |
Regenerate the grammar description file.
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 1 | ||||
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 1 | ||||
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 1 | ||||
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 1 |
4 files changed, 3 insertions, 1 deletions
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 } diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index f6a684bbd7..a143a6c7cf 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -2198,6 +2198,7 @@ ltac2_expr5: [ | REPLACE "let" OPT "rec" LIST1 ltac2_let_clause SEP "with" "in" ltac2_expr6 (* Ltac2 plugin *) | WITH "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" ltac2_expr6 TAG Ltac2 | MOVETO simple_tactic "match" ltac2_expr5 "with" OPT ltac2_branches "end" (* Ltac2 plugin *) +| MOVETO simple_tactic "if" ltac2_expr5 "then" ltac2_expr5 "else" ltac2_expr5 (* Ltac2 plugin *) | DELETE simple_tactic ] diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index c764cb6f37..0638e1753b 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -2586,6 +2586,7 @@ ltac2_expr5: [ | "fun" LIST1 G_LTAC2_input_fun "=>" ltac2_expr6 (* Ltac2 plugin *) | "let" rec_flag LIST1 G_LTAC2_let_clause SEP "with" "in" ltac2_expr6 (* Ltac2 plugin *) | "match" ltac2_expr5 "with" G_LTAC2_branches "end" (* Ltac2 plugin *) +| "if" ltac2_expr5 "then" ltac2_expr5 "else" ltac2_expr5 (* Ltac2 plugin *) | ltac2_expr4 (* Ltac2 plugin *) ] 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 ] |