diff options
| author | Jim Fehrle | 2019-08-05 15:10:32 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2019-11-20 08:53:00 -0800 |
| commit | b4eca882b6692b6374dfff8517f9f5a5cc4970f5 (patch) | |
| tree | ed72a4b0a4cc67c4a988349fb28e0600e7f03ea7 /doc/sphinx/addendum | |
| parent | 4aa756934eb37c6b6d70eddf2b46871bb8ff0956 (diff) | |
Update grammar in the Terms section of Gallina chapter
Update doc_grammar tool
The grammar in the doc is generated semi-automatically with doc_grammar:
- the grammar is automatically extracted from the mlg files
- developer-prepared editing scripts *.mlg_edit modify the extracted
grammar for clarity, simplicity and ordering of productions
- chunks of the resulting grammar are automatically inserted into the
rsts using instructions embedded in the rsts
Running doc_grammar is currently a manual step.
The grammar updates in the rst files have been manually reviewed.
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extraction.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index b568160356..45b3f6f161 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -192,7 +192,7 @@ Disjunctive patterns -------------------- Multiple patterns that share the same right-hand-side can be -factorized using the notation :n:`{+| @mult_pattern}`. For +factorized using the notation :n:`{+| @patterns_comma}`. For instance, :g:`max` can be rewritten as follows: .. coqtop:: in reset diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index 0754145b39..7136cc28d1 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -283,7 +283,7 @@ Notice that in the case of type scheme axiom (i.e. whose type is an arity, that is a sequence of product finished by a sort), then some type variables have to be given (as quoted strings). The syntax is then: -.. cmdv:: Extract Constant @qualid @string ... @string => @string +.. cmdv:: Extract Constant @qualid {+ @string } => @string :undocumented: The number of type variables is checked by the system. For example: diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 4feda5e875..ca5b5e54a7 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -741,7 +741,7 @@ following grammar: : topdown `strategy` (top-down) : hints `ident` (apply hints from hint database) : terms `term` ... `term` (any of the terms) - : eval `redexpr` (apply reduction) + : eval `red_expr` (apply reduction) : fold `term` (unify) : ( `strategy` ) |