diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-04-24 11:59:50 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-05 11:54:03 +0200 |
| commit | d6b7eb3949a499d327a1def31cde62c88f0c1600 (patch) | |
| tree | c1a5d711a3457b89fbb71cc1c31868282eb45155 /doc/sphinx/proof-engine/tactics.rst | |
| parent | e7ad6cb56e5a1dfc6ba6a8afa3445d20b5b86ffa (diff) | |
[sphinx] More reference fixes.
Diffstat (limited to 'doc/sphinx/proof-engine/tactics.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 73961167b..dff3c53bc 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3267,7 +3267,8 @@ See also: :tacn:`autorewrite` for examples showing the use of this tactic. This tactic tries to solve the current goal by a number of standard closing steps. In particular, it tries to close the current goal using the closing tactics - :tacn:`trivial`, reflexivity, symmetry, contradiction and inversion of hypothesis. + :tacn:`trivial`, :tacn:`reflexivity`, :tacn:`symmetry`, :tacn:`contradiction` + and :tacn:`inversion` of hypothesis. If this fails, it tries introducing variables and splitting and-hypotheses, using the closing tactics afterwards, and splitting the goal using :tacn:`split` and recursing. @@ -3278,7 +3279,7 @@ See also: :tacn:`autorewrite` for examples showing the use of this tactic. .. tacv:: now @tactic :name: now - Run :n:`@tac` followed by ``easy``. This is a notation for :n:`@tactic; easy`. + Run :n:`@tactic` followed by :tacn:`easy`. This is a notation for :n:`@tactic; easy`. Controlling automation -------------------------- @@ -3288,7 +3289,7 @@ Controlling automation The hints databases for auto and eauto ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The hints for ``auto`` and ``eauto`` are stored in databases. Each database +The hints for :tacn:`auto` and :tacn:`eauto` are stored in databases. Each database maps head symbols to a list of hints. One can use the command .. cmd:: Print Hint @ident |