diff options
| author | Pierre-Marie Pédrot | 2015-02-27 20:42:44 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-27 20:45:06 +0100 |
| commit | fc1b3ef9d7270938cd83c524aae0383093b7a4b5 (patch) | |
| tree | 9730c1cb313c2b9a510a5030291292353cd41331 /plugins/syntax | |
| parent | 46969b0ece809598b4dd35c688a8ba5237b01efd (diff) | |
Removing the unused field ltacrecvars of tactic internalization.
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions