Override `intuition_solver` instead of redeclaring `intuition`.

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
 

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. *)