diff options
| author | Hugo Herbelin | 2014-10-09 15:36:13 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-09 16:04:42 +0200 |
| commit | 262e7b39f9fe7113ef8180786e4ae6ce69125f87 (patch) | |
| tree | bab6628130e6a047b8029cf56b3d9103a017be1e /plugins/xml | |
| parent | 45566f5651176359aed523b1ddb7e9e5331897f6 (diff) | |
Propagating name of goal to main subgoal in cut and conversion tactics.
Diffstat (limited to 'plugins/xml')
0 files changed, 0 insertions, 0 deletions