diff options
| author | Pierre-Marie Pédrot | 2016-04-15 18:26:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-04-24 19:16:33 +0200 |
| commit | b090942f20ac8854bf227698d31ca1efec492c47 (patch) | |
| tree | 61cdc57146c4151fa743de9b3c2ab59b11722f92 /plugins/pluginsopt.itarget | |
| parent | f3515efc26a693f4c525ad91c37c982f4c96e6ec (diff) | |
Higher-level API for tactic notations.
Diffstat (limited to 'plugins/pluginsopt.itarget')
0 files changed, 0 insertions, 0 deletions