From c1c542a0aec0937bb7605413e2e19aea71c81d43 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 1 May 2023 21:35:44 +0200
Subject: [PATCH] Override `intuition_solver` instead of redeclaring
 `intuition`.

---
 README.md       | 2 ++
 stdpp/tactics.v | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 37f67cb0..9269b34e 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 8b605348..65d7ab7a 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. *)
-- 
GitLab