From c369d5769c1f10058d0809f460341497d7ef7bcd Mon Sep 17 00:00:00 2001
From: Ryan Scott
Date: Mon, 28 Jan 2019 15:26:29 -0500
Subject: Surround "assumption" with :tacn:`` in tactics.rst

---
 doc/sphinx/proof-engine/tactics.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

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
-- 
cgit v1.2.3