aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2017-07-24 15:09:33 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2018-06-15 11:56:52 +0200
commit994f869496b3edd76a903cac16b13e8b6f247d63 (patch)
treeb2bf14d15f2faf8df7a5c6a81be7e55c76248982 /plugins
parent31e13998542941040343cb81787a1d7c865d5b65 (diff)
evd/evarutil: safe [add_unification_pb] interface, taking EConstr's
Avoid adding the same unification problem twice, module evar instantiation.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions