diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-17 20:17:17 +0530 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-17 20:17:17 +0530 |
| commit | 3bcca0aecb368a723d247d1f8b2348790bc87035 (patch) | |
| tree | 81dbfb0613e67109887e9121e3d984bf752aa4ab /library | |
| parent | 014878c3a05365d4af7e3edcfc8d612c45fdf1f3 (diff) | |
Univs: proper printing of global and local universe names (only
printing functions touched in the kernel).
Diffstat (limited to 'library')
| -rw-r--r-- | library/universes.ml | 3 | ||||
| -rw-r--r-- | library/universes.mli | 2 |
2 files changed, 5 insertions, 0 deletions
diff --git a/library/universes.ml b/library/universes.ml index 31bbd1504..79070763e 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -22,6 +22,9 @@ let global_universes = Summary.ref ~name:"Global universe names" let global_universe_names () = !global_universes let set_global_universe_names s = global_universes := s +let pr_with_global_universes l = + try Nameops.pr_id (LMap.find l (snd !global_universes)) + with Not_found -> Level.pr l type universe_constraint_type = ULe | UEq | ULub diff --git a/library/universes.mli b/library/universes.mli index 0053d8f4f..f2f68d329 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -23,6 +23,8 @@ type universe_names = val global_universe_names : unit -> universe_names val set_global_universe_names : universe_names -> unit +val pr_with_global_universes : Level.t -> Pp.std_ppcmds + (** The global universe counter *) val set_remote_new_univ_level : universe_level RemoteCounter.installer |