From 0abade8ca36a68fbd90beb209de7647851416953 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 16 Jun 2016 14:20:10 +0200
Subject: Tentative fix of test-suite file to avoid loop

Looping on jenkins only, couldn't reproduce locally.
To be investigated further.
---
 test-suite/success/bteauto.v | 2 --
 1 file changed, 2 deletions(-)

diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index 21bb10fe17..590f6e191f 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.
 
-- 
cgit v1.2.3