diff options
| author | Matthieu Sozeau | 2015-01-17 20:17:17 +0530 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-01-18 00:16:44 +0530 |
| commit | 237b569dd6539fc1730dbd1dda29f83e24ef8d0c (patch) | |
| tree | 71c1eeaec02da28ae34f8428bab7ddcf7ecc251c /library | |
| parent | 1c0110b40a9009aa6b56fafbf34a04e7ae59de0f (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 31bbd15041..79070763ec 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 0053d8f4f7..f2f68d329c 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 |