diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-01-23 15:55:43 -0500 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-01-23 15:58:31 -0500 |
| commit | 6a046f8d3e33701d70e2a391741e65564cc0554d (patch) | |
| tree | 9c3def82f958dce665d6936656d64dbe0bcf4526 /library/lib.mli | |
| parent | 5cbcc8fd761df0779f6202fef935f07cfef8a228 (diff) | |
Fix bug #4519: oops, global shadowed local universe level bindings.
Diffstat (limited to 'library/lib.mli')
0 files changed, 0 insertions, 0 deletions