diff options
| author | Maxime Dénès | 2017-07-21 17:14:29 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-07-21 17:14:29 +0200 |
| commit | c0fdb912c5e63bb43d6e8dd320e9f5613c6237ff (patch) | |
| tree | ab0e7f43c58a2554f78f317893eb69120dae5dd4 /test-suite/success | |
| parent | f30269579b78d5bf65dcd5db70e341fe9598b274 (diff) | |
| parent | 5b3d0f2cd7a5f480fe24a938e2f6713798c7139a (diff) | |
Merge PR #897: Fix test suite on windows (wrt fake_ide and coq-makefile)
Diffstat (limited to 'test-suite/success')
| -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 1abe14774c..6962e43e7e 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. |