diff options
| -rw-r--r-- | test-suite/success/bteauto.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v index 21bb10fe1..590f6e191 100644 --- a/test-suite/success/bteauto.v +++ b/test-suite/success/bteauto.v @@ -58,8 +58,6 @@ Hint Cut [_* eq_trans eq_sym eq_trans] : core. Goal forall x y z : nat, x = y -> z = y -> x = z. Proof. intros. - Fail Timeout 1 eauto 10000. - typeclasses eauto with core. Qed. |