diff options
| -rw-r--r-- | test-suite/success/eauto.v | 5 |
1 files 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. |