diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-12-29 13:44:11 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-29 13:44:11 +0100 |
commit | 6032ce4f548e88cf341b28dc70d48b9edf6e4f09 (patch) | |
tree | 94b8a23a219ede20d5dda67196ae6b1ed9a7d3b0 /tactics/leminv.mli | |
parent | 3624d943513ff1d79fdadf5b231ffcd3786b16c8 (diff) | |
parent | 9f1d36749529eb66d834d4b417cbc1d8e7cac325 (diff) |
Merge PR #6492: Remove query-in-IDE warning.
Diffstat (limited to 'tactics/leminv.mli')
0 files changed, 0 insertions, 0 deletions