aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorJason Gross2020-05-09 13:39:34 -0400
committerJason Gross2020-05-09 13:39:34 -0400
commit6b223d1d668ecb76aa2609b7d6bb8a19e13136cd (patch)
tree8e67bb69a5b1bf7371c9e80adb75096e0077b03d /plugins
parent3c66c60e52b334482bcfe3d1d97bb77e4d011d18 (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 'plugins')
0 files changed, 0 insertions, 0 deletions