diff --git a/README.md b/README.md
index 37f67cb006fcc34b066425878d79bc51bac8e1d2..9269b34eea56db4876dbecf31796f85f3d428fca 100644
--- a/README.md
+++ b/README.md
@@ -36,6 +36,8 @@ Notably:
 * It blocks `simpl` on all operations involving integers `Z` (by setting
   `Arguments op : simpl never`). We do this because `simpl` tends to expose
   the internals of said operations (e.g. try `simpl` on `Z.of_nat (S n) + y`).
+* It sets `intuition_solver` to `auto`. The default is `auto with *`, which is
+  very expensive.
 
 ## Prerequisites
 
diff --git a/stdpp/tactics.v b/stdpp/tactics.v
index 8b60534840bbb3cae8550757f62c433e0f71e646..65d7ab7a484c1d3089ec2779be40d94a0f824648 100644
--- a/stdpp/tactics.v
+++ b/stdpp/tactics.v
@@ -29,7 +29,7 @@ be very bad, so use with care! *)
 (** The tactic [intuition] expands to [intuition auto with *] by default. This
 is rather inefficient when having big hint databases, or expensive [Hint Extern]
 declarations as the ones above. *)
-Tactic Notation "intuition" := intuition auto.
+Ltac intuition_solver ::= auto.
 
 (** The [fast_reflexivity] tactic only works on syntactically equal terms. It
 can be used to avoid expensive failing unification. *)