diff options
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` ) |