From 7e55f4813d5173d659482a6899c3f97c5346a682 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 15 Nov 2020 15:30:28 +0100
Subject: Document the new export locality for the remaining hint commands.

---
 doc/sphinx/proofs/automatic-tactics/auto.rst | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'doc/sphinx')

diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst
index e6dc6f6c51..485b92342d 100644
--- a/doc/sphinx/proofs/automatic-tactics/auto.rst
+++ b/doc/sphinx/proofs/automatic-tactics/auto.rst
@@ -280,9 +280,7 @@ automatically created.
      sections.
 
    + :attr:`export` are visible from other modules when they import the current
-     module. Requiring it is not enough. This attribute is only effective for
-     the :cmd:`Hint Resolve`, :cmd:`Hint Immediate`, :cmd:`Hint Unfold` and
-     :cmd:`Hint Extern` variants of the command.
+     module. Requiring it is not enough.
 
    + :attr:`global` hints are made available by merely requiring the current
      module.
-- 
cgit v1.2.3