diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-01 22:50:37 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-01 22:52:08 +0200 |
| commit | 4c97e4ce19ca4c387039cfdcb4f24658100230b0 (patch) | |
| tree | 8e6367b1936d842b3e56283abc25de2342452884 /pretyping | |
| parent | 3d2582eeb492fb21b7136016bf4c1a0463dc15c2 (diff) | |
Add toplevel commands to declare global universes and constraints.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 7 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 13 |
2 files changed, 15 insertions, 5 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index a7a8bf5be..92a29fce7 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -370,7 +370,12 @@ let detype_sort = function | Type u -> GType (if !print_universes - then Some (Pp.string_of_ppcmds (Univ.Universe.pr u)) + then + let _, map = Universes.global_universe_names () in + let pr_level u = + try Nameops.pr_id (Univ.LMap.find u map) with Not_found -> Univ.Level.pr u + in + Some (Pp.string_of_ppcmds (Univ.Universe.pr_with pr_level u)) else None) type binder_kind = BProd | BLambda | BLetIn diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index c8c1d0e21..9609a959b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -96,10 +96,15 @@ let ((constr_in : constr -> Dyn.t), let interp_universe_name evd = function | None -> new_univ_level_variable univ_rigid evd | Some s -> - try let level = Evd.universe_of_name evd s in - evd, level - with Not_found -> - new_univ_level_variable ~name:s univ_rigid evd + try + let id = try Id.of_string s with _ -> raise Not_found in + let names, _ = Universes.global_universe_names () in + evd, Idmap.find id names + with Not_found -> + try let level = Evd.universe_of_name evd s in + evd, level + with Not_found -> + new_univ_level_variable ~name:s univ_rigid evd let interp_sort evd = function | GProp -> evd, Prop Null |