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 /doc/sphinx | |
| parent | 2559f0474c8cd66b5020524d1e758ea7a19bc8fb (diff) | |
Regenerate the grammar description file.
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 1 |
1 files changed, 0 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 } |