diff options
| author | Pierre-Marie Pédrot | 2016-04-25 10:00:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-04-25 10:12:31 +0200 |
| commit | 27d4a57975ab5919d81f9951b430a35d1067e846 (patch) | |
| tree | d49c0258800cf1cefbe2f56a89fcbb9426364107 /plugins/pluginsopt.itarget | |
| parent | 3f5aa726ea075765ae7ec03d7f34f795cc6a1bc9 (diff) | |
Factorizing code in tactic notations.
Diffstat (limited to 'plugins/pluginsopt.itarget')
0 files changed, 0 insertions, 0 deletions