From 6876a3cd9dd1d7c94f9d387904c6a6f6d88c31f8 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 28 May 2016 17:12:06 +0200
Subject: eauto: fix test-suite file

Now that typeclasses eauto uses the new eauto.
---
 test-suite/success/eauto.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index 26a4c4d916..17b3aaef2f 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -157,9 +157,8 @@ Hint Extern 0 { x : _ & _ } => simple refine (existT _ _ _) : typeclass_instance
 
 Definition trivial a (H : Foo a) : {b : myType & Qux b}. 
 Proof.
-  Fail typeclasses eauto with typeclass_instances.
-  fulleauto 4.
+  Time fulleauto 10.
   Undo. Set Typeclasses Iterative Deepening.
-  fulleauto.
+  Time fulleauto.
 Defined.
 
-- 
cgit v1.2.3