aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/eauto.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success/eauto.v')
-rw-r--r--test-suite/success/eauto.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index c9c7c611c..4db547f4e 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -117,7 +117,7 @@ Lemma simpl_plus_l_rr1 :
Undo.
Set Typeclasses Debug.
Set Typeclasses Iterative Deepening.
- Time typeclasses eauto 2 with nocore. Show Proof.
+ Time typeclasses eauto 6 with nocore. Show Proof.
Undo.
Time eauto. (* does EApply H *)
Qed.