From 3bcca0aecb368a723d247d1f8b2348790bc87035 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 17 Jan 2015 20:17:17 +0530 Subject: Univs: proper printing of global and local universe names (only printing functions touched in the kernel). --- library/universes.ml | 3 +++ library/universes.mli | 2 ++ 2 files changed, 5 insertions(+) (limited to 'library') 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 -- cgit v1.2.3