diff options
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. |