diff options
Diffstat (limited to 'doc/sphinx/proofs')
| -rw-r--r-- | doc/sphinx/proofs/automatic-tactics/auto.rst | 13 | ||||
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 6 |
2 files changed, 10 insertions, 9 deletions
diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst index d7228a3907..30f7be5f13 100644 --- a/doc/sphinx/proofs/automatic-tactics/auto.rst +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -273,18 +273,21 @@ Creating Hints :cmd:`Import` or :cmd:`Require` the current module. + :attr:`export` hints are visible from other modules when they :cmd:`Import` the current - module, but not when they only :cmd:`Require` it. This attribute is supported by - all `Hint` commands except for :cmd:`Hint Rewrite`. + module, but not when they only :cmd:`Require` it. + :attr:`global` hints are visible from other modules when they :cmd:`Import` or :cmd:`Require` the current module. + .. versionadded:: 8.14 + + The :cmd:`Hint Rewrite` now supports locality attributes like other `Hint` commands. + .. deprecated:: 8.13 The default value for hint locality will change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality will trigger a deprecation - warning. We recommend you use :attr:`export` whenever possible. + release. Hints added outside of sections without an explicit + locality are now deprecated. We recommend using :attr:`export` + where possible. The `Hint` commands are: diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index 5b9304102c..0a4a48555f 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -883,10 +883,8 @@ the conversion in hypotheses :n:`{+ @ident}`. Conversion tactics applied to hypotheses ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. tacn:: @tactic in {+, @ident} - - Applies :token:`tactic` (any of the conversion tactics listed in this - section) to the hypotheses :n:`{+ @ident}`. + The form :n:`@tactic in {+, @ident }` applies :token:`tactic` (any of the + conversion tactics listed in this section) to the hypotheses :n:`{+ @ident}`. If :token:`ident` is a local definition, then :token:`ident` can be replaced by :n:`type of @ident` to address not the body but the type of the local |