diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-15 15:46:30 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-24 19:18:56 +0100 |
| commit | d437078a4ca82f7ca6d19be5ee9452359724f9a0 (patch) | |
| tree | 628fd2161dcc0fcfabe9499669ee932d7878b63d /pretyping | |
| parent | 485a0a6280abbef62f7e2c2bfbaf3b73d67bbdaf (diff) | |
Use Maps and ids for universe binders
Before sometimes there were lists and strings.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 25 | ||||
| -rw-r--r-- | pretyping/univdecls.ml | 2 |
2 files changed, 13 insertions, 14 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e3470b0f1..ffbc21a5e 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -181,9 +181,8 @@ let interp_universe_level_name ~anon_rigidity evd (loc, s) = match s with | Anonymous -> new_univ_level_variable ?loc anon_rigidity evd - | Name s -> - let s = Id.to_string s in - let names, _ = Global.global_universe_names () in + | Name id -> + let s = Id.to_string id in if CString.string_contains ~where:s ~what:"." then match List.rev (CString.split '.' s) with | [] -> anomaly (str"Invalid universe name " ++ str s ++ str".") @@ -197,17 +196,17 @@ let interp_universe_level_name ~anon_rigidity evd (loc, s) = in evd, level else try - let level = Evd.universe_of_name evd s in - evd, level + let level = Evd.universe_of_name evd id in + evd, level with Not_found -> - try - let id = try Id.of_string s with _ -> raise Not_found in - evd, snd (Id.Map.find id names) - with Not_found -> - if not (is_strict_universe_declarations ()) then - new_univ_level_variable ?loc ~name:s univ_rigid evd - else user_err ?loc ~hdr:"interp_universe_level_name" - (Pp.(str "Undeclared universe: " ++ str s)) + try + let names, _ = Global.global_universe_names () in + evd, snd (Id.Map.find id names) + with Not_found -> + if not (is_strict_universe_declarations ()) then + new_univ_level_variable ?loc ~name:id univ_rigid evd + else user_err ?loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared universe: " ++ str s)) let interp_universe ?loc evd = function | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml index 5576e33f4..a5266125a 100644 --- a/pretyping/univdecls.ml +++ b/pretyping/univdecls.ml @@ -31,7 +31,7 @@ let interp_univ_constraints env evd cstrs = user_err ~hdr:"interp_constraint" (str "Cannot declare constraints on anonymous universes") | GType (Some (loc, Name id)) -> - try loc, Evd.universe_of_name evd (Id.to_string id) + try loc, Evd.universe_of_name evd id with Not_found -> user_err ?loc ~hdr:"interp_constraint" (str "Undeclared universe " ++ Id.print id) in |