Fix text describing selective import: not available for tactics. (#29)

coq · Jul 4, 2024 · 60969b1 · 60969b1
1 parent fc167a7
commit 60969b1
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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.