Small API additions to kernel/univ

- allow viewing the internal representation of uglobal and universe
  (with universe, this replaces the "map" function. I kept exists and
  for_all as they felt somewhat convenient)
- add universe set and map modules (currently unused but they're natural)

1 files changed, 1 insertions, 1 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 037006bc47..b042437a22 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -696,7 +696,7 @@ let detype_universe sigma u =
       if Univ.Level.is_set l then GSet else
       GType (hack_qualid_of_univ_level sigma l) in
     (s, n) in
-  Univ.Universe.map fn u
+  List.map fn (Univ.Universe.repr u)
 
 let detype_sort sigma = function
   | SProp -> UNamed [GSProp,0]