From d6b7eb3949a499d327a1def31cde62c88f0c1600 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 24 Apr 2018 11:59:50 +0200 Subject: [sphinx] More reference fixes. --- doc/sphinx/proof-engine/tactics.rst | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'doc/sphinx/proof-engine/tactics.rst') 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 -- cgit v1.2.3