diff options
| author | Pierre-Marie Pédrot | 2017-05-16 18:03:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-05-19 15:17:31 +0200 |
| commit | df1c50b36f4927fdf64a3ed99a4a077f5175ac5e (patch) | |
| tree | 946d7699ec1b609463883de759f3dc408d2e65a5 /plugins | |
| parent | a16d9c10b874a38fd4901e7d946d975ad49592c5 (diff) | |
Removing dead code in Ltac2, and cleaning up a bit.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions