diff options
| author | Jim Fehrle | 2020-09-12 20:54:22 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2021-03-08 11:48:20 -0800 |
| commit | 0d33024ff79c38d52fde49e23d0e45d9c22eefbe (patch) | |
| tree | 864068cd317abebcbc0a3466a1365258729fbc40 /doc/sphinx/proofs/automatic-tactics | |
| parent | fb0666d50e1fe95ad2325f4ef2cc9fdd2666ac8a (diff) | |
Convert 2nd part of rewriting chapter to prodn
Diffstat (limited to 'doc/sphinx/proofs/automatic-tactics')
| -rw-r--r-- | doc/sphinx/proofs/automatic-tactics/auto.rst | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst index 30f7be5f13..d9945dd920 100644 --- a/doc/sphinx/proofs/automatic-tactics/auto.rst +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -139,14 +139,13 @@ Programmable proof search Like :tacn:`eauto`, but uses a `breadth-first search <https://en.wikipedia.org/wiki/Breadth-first_search>`_. -.. tacn:: autounfold {? @hintbases } {? @occurrences } +.. tacn:: autounfold {? @hintbases } {? @simple_occurrences } Unfolds constants that were declared through a :cmd:`Hint Unfold` in the given databases. - :n:`@occurrences` - Performs the unfolding in the specified occurrences. The :n:`at @occs_nums` - clause of :n:`@occurrences` is not supported. + :n:`@simple_occurrences` + Performs the unfolding in the specified occurrences. .. tacn:: autorewrite {? * } with {+ @ident } {? @occurrences } {? using @ltac_expr } @@ -376,6 +375,9 @@ Creating Hints discrimination network to relax or constrain it in the case of discriminated databases. + .. exn:: Cannot coerce @qualid to an evaluable reference. + :undocumented: + .. cmd:: Hint {| Constants | Variables } {| Transparent | Opaque } {? : {+ @ident } } :name: Hint Constants; Hint Variables |