diff options
| author | Jason Gross | 2020-05-09 13:39:34 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-05-09 13:39:34 -0400 |
| commit | 6b223d1d668ecb76aa2609b7d6bb8a19e13136cd (patch) | |
| tree | 8e67bb69a5b1bf7371c9e80adb75096e0077b03d /test-suite | |
| parent | 3c66c60e52b334482bcfe3d1d97bb77e4d011d18 (diff) | |
Revert "[with_strategy] Fix for coqchk"
This reverts commit 3c66c60e52b334482bcfe3d1d97bb77e4d011d18.
We instead add a warning in the manual and a kludge in the test-suite.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/with_strategy.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/success/with_strategy.v b/test-suite/success/with_strategy.v index e0d0252a47..077b57c87f 100644 --- a/test-suite/success/with_strategy.v +++ b/test-suite/success/with_strategy.v @@ -572,3 +572,6 @@ Goal id 0 = 0. (assert_succeeds unfold_id))))))))))). reflexivity. Qed. + +(* Fake out coqchk to work around what is essentially COQBUG(https://github.com/coq/coq/issues/12200) *) +Reset Initial. |