From 458cf1324163821b60ab0b731a60bb1977576d9f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 27 Jan 2020 13:29:18 +0100
Subject: 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)
---
 pretyping/detyping.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

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]
-- 
cgit v1.2.3