diff options
| author | Matthieu Sozeau | 2014-09-08 10:23:12 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-08 17:09:43 +0200 |
| commit | 26a79004e47bbdc97df61015ce7e944eef14ac71 (patch) | |
| tree | 1f24c9acbb73cd63dcc689222b965f245767137e /pretyping/detyping.ml | |
| parent | 89ad50f4d7e1312539995ced3a632821bf6af7c5 (diff) | |
Parsing of Type@{max(i,j)}.
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index bdec8307a1..3a355b91a9 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -374,9 +374,9 @@ let detype_sort = function let _, map = Universes.global_universe_names () in let pr_level u = try Nameops.pr_id (Univ.LMap.find u map) with Not_found -> Univ.Level.pr u - in - Some (Pp.string_of_ppcmds (Univ.Universe.pr_with pr_level u)) - else None) + in + [Pp.string_of_ppcmds (Univ.Universe.pr_with pr_level u)] + else []) type binder_kind = BProd | BLambda | BLetIn |