diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-28 22:28:21 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-25 14:18:35 +0100 |
| commit | f8e639f3b81ae142f5b529be1ad90210fc259375 (patch) | |
| tree | d73251d05312b34ba8f6e38387c3a07372603588 /pretyping/pretyping.ml | |
| parent | d071eac98b7812ac5c03004b438022900885d874 (diff) | |
Fix interpretation of global universes in univdecl constraints.
Also nicer error when the constraints are impossible.
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 30 |
1 files changed, 23 insertions, 7 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index ffbc21a5e..a9bff5bf6 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -177,6 +177,14 @@ let _ = optwrite = (:=) Universes.set_minimization }) (** Miscellaneous interpretation functions *) +let interp_known_universe_level evd id = + try + let level = Evd.universe_of_name evd id in + level + with Not_found -> + let names, _ = Global.global_universe_names () in + snd (Id.Map.find id names) + let interp_universe_level_name ~anon_rigidity evd (loc, s) = match s with | Anonymous -> @@ -195,13 +203,7 @@ let interp_universe_level_name ~anon_rigidity evd (loc, s) = with UGraph.AlreadyDeclared -> evd in evd, level else - try - let level = Evd.universe_of_name evd id in - evd, level - with Not_found -> - try - let names, _ = Global.global_universe_names () in - evd, snd (Id.Map.find id names) + try evd, interp_known_universe_level evd id with Not_found -> if not (is_strict_universe_declarations ()) then new_univ_level_variable ?loc ~name:id univ_rigid evd @@ -218,6 +220,15 @@ let interp_universe ?loc evd = function (evd', Univ.sup u (Univ.Universe.make l))) (evd, Univ.Universe.type0m) l +let interp_known_level_info ?loc evd = function + | None | Some (_, Anonymous) -> + user_err ?loc ~hdr:"interp_known_level_info" + (str "Anonymous universes not allowed here.") + | Some (loc, Name id) -> + try interp_known_universe_level evd id + with Not_found -> + user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Id.print id) + let interp_level_info ?loc evd : Misctypes.level_info -> _ = function | None -> new_univ_level_variable ?loc univ_rigid evd | Some (loc,s) -> interp_universe_level_name ~anon_rigidity:univ_flexible evd (Loc.tag ?loc s) @@ -466,6 +477,11 @@ let pretype_id pretype k0 loc env evdref lvar id = (*************************************************************************) (* Main pretyping function *) +let interp_known_glob_level ?loc evd = function + | GProp -> Univ.Level.prop + | GSet -> Univ.Level.set + | GType s -> interp_known_level_info ?loc evd s + let interp_glob_level ?loc evd : Misctypes.glob_level -> _ = function | GProp -> evd, Univ.Level.prop | GSet -> evd, Univ.Level.set |