From 89b3547b231851c739c58c20e2f19073a5cb4c5b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 19 Jul 2016 17:02:53 -0700 Subject: 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 --- src/ModularArithmetic/ModularBaseSystemProofs.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/ModularArithmetic') 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. } -- cgit v1.2.3