diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-27 11:37:11 +0200 |
|---|---|---|
| committer |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-07-20 15:40:48 +0200 |
| commit | 8fdc88a79837c70857c51fcb3e0930f1ac3e9c8a (patch) | |
| tree | f378a5eb12e72e19955b41c62baa031944277a53 /test-suite/success/Hints.v | |
| parent | 9682fea9f71477af58681735d8829507991d27c5 (diff) | |
Remove non-terminating Timeout tests from Hints.v.
Diffstat (limited to 'test-suite/success/Hints.v')
| -rw-r--r-- | test-suite/success/Hints.v | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index 1abe14774..6962e43e7 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -37,7 +37,6 @@ Hint Resolve predf | 0 : predconv. Goal exists n, pred n. eexists. - Fail Timeout 1 typeclasses eauto with pred. Set Typeclasses Filtered Unification. Set Typeclasses Debug Verbosity 2. (* predf is not tried as it doesn't match the goal *) @@ -80,8 +79,6 @@ Qed. (** The other way around: goal contains redexes instead of instances *) Goal exists n, pred (0 + n). eexists. - (* predf is applied indefinitely *) - Fail Timeout 1 typeclasses eauto with pred. (* pred0 (pred _) matches the goal *) typeclasses eauto with predconv. Qed. @@ -169,8 +166,6 @@ Instance foo f : E (id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ f ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id). Proof. - Fail Timeout 1 apply _. (* 3.7s *) - Hint Cut [_* (a_is_b | b_is_c | c_is_d | d_is_e) (a_compose | b_compose | c_compose | d_compose | e_compose)] : typeclass_instances. |