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 /dev/tools | |
| 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 'dev/tools')
0 files changed, 0 insertions, 0 deletions