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

1 files changed, 1 insertions, 1 deletions

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.
     }