aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorMatthieu Sozeau2014-12-14 18:54:24 +0100
committerMatthieu Sozeau2014-12-14 19:06:14 +0100
commit2db658105f8ed20ca2153271b339c777b79da406 (patch)
tree9aedc88d0c0338c98b9f68300f16f52f2f0aa44b /lib
parente117099919cb0a474cad4fe2a6d15165b2520760 (diff)
Fix merging of name maps in union of universe contexts.
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions