diff options
| author | Pierre-Marie Pédrot | 2014-04-22 12:11:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-04-22 12:20:27 +0200 |
| commit | 17b84de9ec0b14006dda0e1588f04a830ac5995f (patch) | |
| tree | 9722282adcefd3d97f0de76ec31f0405c826359b /plugins/syntax/string_syntax_plugin.mllib | |
| parent | f76c0b3b89ce433de5cad7d35c437ce26f1e7477 (diff) | |
Removing the compatibility layer from Leminv. Also removed an undocumented
variant of the Derive Inversion command which took the current goal as the
targeted inductive. It was unused in the contribs and it seemed rather
bad from the STM point of view, as it generated a lemma inside a proof.
Diffstat (limited to 'plugins/syntax/string_syntax_plugin.mllib')
0 files changed, 0 insertions, 0 deletions