aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-09 15:36:13 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-09 16:04:42 +0200
commit262e7b39f9fe7113ef8180786e4ae6ce69125f87 (patch)
treebab6628130e6a047b8029cf56b3d9103a017be1e /plugins
parent45566f5651176359aed523b1ddb7e9e5331897f6 (diff)
Propagating name of goal to main subgoal in cut and conversion tactics.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions