Work around bad design in Coq

This is https://coq.inria.fr/bugs/show_bug.cgi?id=4949, [intuition]
should not use [auto with *] by default

2 files changed, 3 insertions, 1 deletions

diff --git a/folkwisdom.md b/folkwisdom.md
index 3c8d92036..d6d65f12e 100644
--- a/folkwisdom.md
+++ b/folkwisdom.md
@@ -280,6 +280,8 @@ Considerations not (yet) covered in this document include the following:
   - how to write tactics that are debuggable
   - how to write tactics that are robust against small changes
   - reification: ltac, typeclasses, canonical structures (maybe reference an existing document)
+  - how `intuition` should never be used because it calls `auto with *`, which
+    leads to fragile documents, and `intuition auto` should be used instead
 - performance of proofs and proof checking
   - `simpl`, `cbn`, `cbv`
   - `Qed slowness, `change` vs `rewrite`
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index c3b1b76b4..c06dcdf98 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -127,7 +127,7 @@ Section PseudoMersenneProofs.
 
   Lemma add_rep : forall u v x y, u ~= x -> v ~= y -> BaseSystem.add u v ~= (x+y)%F.
   Proof.
-    autounfold; intuition. {
+    autounfold; intuition auto. {
       unfold add.
       auto using add_same_length.
     }