diff options
| author | Théo Zimmermann | 2019-01-29 09:51:20 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-01-29 09:51:20 +0100 |
| commit | 10253b1e744e8075b708a9fe328f49c06bbc3fef (patch) | |
| tree | 9ce2cbb0384e8c92a6a85c986fd50e140009e58b | |
| parent | 0a75fb2209643cb35285f584f3ee313242c6d3e7 (diff) | |
| parent | c369d5769c1f10058d0809f460341497d7ef7bcd (diff) | |
Merge PR #9424: Surround "assumption" with :tacn:`` in tactics.rst
Reviewed-by: jfehrle
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 250d9c3a8a..7eef504ea9 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3388,7 +3388,7 @@ Automation :name: auto This tactic implements a Prolog-like resolution procedure to solve the - current goal. It first tries to solve the goal using the assumption + current goal. It first tries to solve the goal using the :tacn:`assumption` tactic, then it reduces the goal to an atomic one using intros and introduces the newly generated hypotheses as hints. Then it looks at the list of tactics associated to the head symbol of the goal and |