From 6a046f8d3e33701d70e2a391741e65564cc0554d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 23 Jan 2016 15:55:43 -0500 Subject: Fix bug #4519: oops, global shadowed local universe level bindings. --- pretyping/pretyping.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'pretyping/pretyping.ml') 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 -- cgit v1.2.3