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 /pretyping | |
| parent | 5cbcc8fd761df0779f6202fef935f07cfef8a228 (diff) | |
Fix bug #4519: oops, global shadowed local universe level bindings.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index ac0104d9f..b33084a42 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -138,12 +138,12 @@ let interp_universe_level_name evd (loc,s) = in evd, level else try - let id = - try Id.of_string s with _ -> raise Not_found in - evd, Idmap.find id names + let level = Evd.universe_of_name evd s in + evd, level with Not_found -> - try let level = Evd.universe_of_name evd s in - evd, level + try + let id = try Id.of_string s with _ -> raise Not_found in + evd, Idmap.find id names with Not_found -> if not (is_strict_universe_declarations ()) then new_univ_level_variable ~name:s univ_rigid evd |