diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-06-15 00:59:24 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-06-16 18:21:08 +0200 |
| commit | d7283b37ddba514d29b977866058dabf45b464e7 (patch) | |
| tree | e0a04f84465232bf8b7a49e1ecfbed5dd2d0dc8a /test-suite/success/bteauto.v | |
| parent | cad3fa50357d97e309e9d4fc2a877991c83649d8 (diff) | |
Cleanup and refactoring
Diffstat (limited to 'test-suite/success/bteauto.v')
| -rw-r--r-- | test-suite/success/bteauto.v | 41 |
1 files changed, 5 insertions, 36 deletions
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v index 4b28da19d..21bb10fe1 100644 --- a/test-suite/success/bteauto.v +++ b/test-suite/success/bteauto.v @@ -58,7 +58,7 @@ 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 1000. + Fail Timeout 1 eauto 10000. typeclasses eauto with core. Qed. @@ -94,11 +94,11 @@ Check (eqp 0%nat 0). (* Defaulting *) Check (fun x y => eqp x y). - -Hint Mode Equality + : typeclass_instances. - (* No more defaulting, reduce "trigger-happiness" *) -Fail Definition ambiguous x y := eqp x y. +Definition ambiguous x y := eqp x y. + +Hint Mode Equality ! : typeclass_instances. +Fail Definition ambiguous' x y := eqp x y. Definition nonambiguous (x y : nat) := eqp x y. (** Typical looping instances with defaulting: *) @@ -119,36 +119,6 @@ Hint Mode SomeProp + + : typeclass_instances. Check prf. Check (fun H : SomeProp plus => _ : SomeProp (flip plus)). - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - (** Iterative deepening / breadth-first search *) Module IterativeDeepening. @@ -164,7 +134,6 @@ Module IterativeDeepening. Goal C -> A. intros. - Set Typeclasses Debug. Fail Timeout 1 typeclasses eauto. Set Typeclasses Iterative Deepening. Fail typeclasses eauto 1. |