aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorHugo Herbelin2014-12-09 14:10:45 +0100
committerHugo Herbelin2014-12-11 18:34:04 +0100
commitccc7d1ec570e691a6824d9e6f43665f2eb4a1e3f (patch)
treecf8be55eba3f902daeaf75694a4dfcdc94d17d67 /plugins
parent34cb1f6491017e4ed1a509f6b83b88a812ac425f (diff)
Fine-tuning unification error (using OccurCheck in evarconv).
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions