diff options
| author | Matthieu Sozeau | 2016-05-28 17:12:06 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-16 18:21:08 +0200 |
| commit | 6876a3cd9dd1d7c94f9d387904c6a6f6d88c31f8 (patch) | |
| tree | 0049015fabfc1f157fe6ff02925067a701eaeffb | |
| parent | 855143c550cad6694f77a782d1056b07f8197bd3 (diff) | |
eauto: fix test-suite file
Now that typeclasses eauto uses the new eauto.
| -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. |