aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssrmatching
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-09-04 08:33:51 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-09-16 15:30:09 +0200
commit1a1af4f2119715245b8d4488664a8b57f4bdce08 (patch)
treec76d6383b9761ce5042b2062efd381057cdc5600 /plugins/ssrmatching
parent753248c145cdac846528d809a1f085c18408e17f (diff)
Adding variants enter_one and refine_one which assume that exactly one
goal is under focus and which support returning a relevant output.
Diffstat (limited to 'plugins/ssrmatching')
0 files changed, 0 insertions, 0 deletions