From 60969b1235a9c41359166089bc913de102ee4b1f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= <theo.zimmermann@telecom-paris.fr>
Date: Thu, 4 Jul 2024 06:27:23 +0200
Subject: [PATCH] Fix text describing selective import: not available for
 tactics. (#29)

---
 src/RequireImportTutorial.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/RequireImportTutorial.v b/src/RequireImportTutorial.v
index f4bac20..853ce44 100644
--- a/src/RequireImportTutorial.v
+++ b/src/RequireImportTutorial.v
@@ -643,7 +643,7 @@ Compute 1 !!.
     The other import categories correspond to what we mentioned before, namely:
     [hints], [canonicals], [ltac.notations] and [ltac2.notations]. *)
 
-(** We can also select which constants, tactics and abbreviations are available
+(** We can also select which constants and abbreviations are available
     by their short names: *)
 Import Baz(almost_b, b_rel, add_two).
 Check almost_b.