From f91f2ac64fbc7035c77592195c67050640abc3cb Mon Sep 17 00:00:00 2001
From: Paolo G. Giarrusso
Date: Sat, 11 Jul 2020 18:10:18 +0200
Subject: tactics.rst: `Require A` is enough for `A`'s hints

As the text says later:
> Hints should only be made available when the module they are defined in is imported, not just required.---
 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 4af3ebc47b..25c4de7389 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -4162,7 +4162,7 @@ Hint locality
 Hints provided by the ``Hint`` commands are erased when closing a section.
 Conversely, all hints of a module ``A`` that are not defined inside a
 section (and not defined with option ``Local``) become available when the
-module ``A`` is imported (using e.g. ``Require Import A.``).
+module ``A`` is required (using e.g. ``Require A.``).
 
 As of today, hints only have a binary behavior regarding locality, as
 described above: either they disappear at the end of a section scope,
-- 
cgit v1.2.3