diff --git a/theories/tactics.v b/theories/tactics.v
index 2baea53c02596cc1c6053523658fa554a585345c..79a5be4489f42b98d1c59b5e351031ca9a200c40 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -27,7 +27,7 @@ Global Hint Extern 1001 => progress subst : subst. (** backtracking on this one
 be very bad, so use with care! *)
 
 (** The tactic [intuition] expands to [intuition auto with *] by default. This
-is rather efficient when having big hint databases, or expensive [Hint Extern]
+is rather inefficient when having big hint databases, or expensive [Hint Extern]
 declarations as the ones above. *)
 Tactic Notation "intuition" := intuition auto.