diff options
| author | Jim Fehrle | 2019-07-21 14:28:10 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2019-07-28 14:43:26 -0700 |
| commit | e33f5d2d3930ab7818abccef4bf2326c72b348eb (patch) | |
| tree | dcc6c734a8ab85fae627851b9591bde48d3e69d0 /doc/sphinx/proof-engine/ltac2.rst | |
| parent | cd6fc50854285f02bf151e94bdfb819988531fd2 (diff) | |
Update documentation on tokens, use "int" and "num"
for integers and natural nums
Diffstat (limited to 'doc/sphinx/proof-engine/ltac2.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 3036648b08..ceaa2775bf 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -179,7 +179,7 @@ constructions from ML. : let `ltac2_var` := `ltac2_term` in `ltac2_term` : let rec `ltac2_var` := `ltac2_term` in `ltac2_term` : match `ltac2_term` with `ltac2_branch` ... `ltac2_branch` end - : `integer` + : `int` : `string` : `ltac2_term` ; `ltac2_term` : [| `ltac2_term` ; ... ; `ltac2_term` |] @@ -670,7 +670,7 @@ A scope is a name given to a grammar entry used to produce some Ltac2 expression at parsing time. Scopes are described using a form of S-expression. .. prodn:: - ltac2_scope ::= {| @string | @integer | @lident ({+, @ltac2_scope}) } + ltac2_scope ::= {| @string | @int | @lident ({+, @ltac2_scope}) } A few scopes contain antiquotation features. For sake of uniformity, all antiquotations are introduced by the syntax :n:`$@lident`. @@ -719,7 +719,7 @@ The following scopes are built-in. + parses a Ltac2 expression at the next level and return it as is. -- :n:`tactic(n = @integer)`: +- :n:`tactic(n = @int)`: + parses a Ltac2 expression at the provided level :n:`n` and return it as is. @@ -760,7 +760,7 @@ Notations The Ltac2 parser can be extended by syntactic notations. -.. cmd:: Ltac2 Notation {+ {| @lident (@ltac2_scope) | @string } } {? : @integer} := @ltac2_term +.. cmd:: Ltac2 Notation {+ {| @lident (@ltac2_scope) | @string } } {? : @int} := @ltac2_term :name: Ltac2 Notation A Ltac2 notation adds a parsing rule to the Ltac2 grammar, which is expanded |