diff options
| author | Pierre-Marie Pédrot | 2020-01-29 15:47:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-01-29 15:47:17 +0100 |
| commit | d135b30704dff9ce1dce700f49a41e4089153d8f (patch) | |
| tree | 19b7173c01a7d02c7a50676c5a2488f3535905c0 /pretyping | |
| parent | a510adb17481ae2c007463c083f562725cda9896 (diff) | |
| parent | 458cf1324163821b60ab0b731a60bb1977576d9f (diff) | |
Merge PR #11455: Small API additions to kernel/univ
Reviewed-by: ppedrot
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 2 |
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] |