diff options
| author | Pierre-Marie Pédrot | 2020-06-20 13:11:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-24 15:38:24 +0200 |
| commit | 43b1742b2d7da56315fdc8e99c730fb456259cd5 (patch) | |
| tree | dadc005055714838a2b5adae87bcc5dca2a3d139 /tactics/tactics.ml | |
| parent | 82485e9f2a36a7a52a56622a553817436636b00b (diff) | |
Remove dead code in branch_args.
Diffstat (limited to 'tactics/tactics.ml')
0 files changed, 0 insertions, 0 deletions