diff options
| author | Matthieu Sozeau | 2014-12-14 18:54:24 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-12-14 19:06:14 +0100 |
| commit | 2db658105f8ed20ca2153271b339c777b79da406 (patch) | |
| tree | 9aedc88d0c0338c98b9f68300f16f52f2f0aa44b /lib/util.ml | |
| parent | e117099919cb0a474cad4fe2a6d15165b2520760 (diff) | |
Fix merging of name maps in union of universe contexts.
Diffstat (limited to 'lib/util.ml')
0 files changed, 0 insertions, 0 deletions