diff options
| author | Jason Gross | 2020-04-25 13:33:39 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-05-09 13:03:05 -0400 |
| commit | ee3b91fe06c72a8ffe92d31a7e40fe54cd71f746 (patch) | |
| tree | 6f3f83b64e649154afe3c62071054979403b9228 /test-suite | |
| parent | 33388d18f0165369a565cd5ca5b6eb153899271e (diff) | |
Elaborate with_strategy warning
As per https://github.com/coq/coq/pull/12129#issuecomment-619389803
Note that we need to work around #12179 in doc of with_strategy
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/with_strategy.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/success/with_strategy.v b/test-suite/success/with_strategy.v index bacea3549f..4f761fb470 100644 --- a/test-suite/success/with_strategy.v +++ b/test-suite/success/with_strategy.v @@ -138,6 +138,17 @@ Goal id 0 = 0. reflexivity. Time Timeout 5 Defined. +(* test that it works even with [Qed] *) +Goal id 0 = 0. +Proof using Type. + Time Timeout 5 + abstract + (with_strategy + expand [id] + assert (id (fact 100) = fact 100) by abstract reflexivity; + reflexivity). +Time Timeout 5 Qed. + (* check that module substitutions happen correctly *) Module F. Definition id {T} := @id T. |