diff options
| -rw-r--r-- | intf/misctypes.mli | 2 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 6 | ||||
| -rw-r--r-- | printing/ppconstr.ml | 2 |
3 files changed, 7 insertions, 3 deletions
diff --git a/intf/misctypes.mli b/intf/misctypes.mli index b9f5a6dbe2..e8164c02d6 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -37,7 +37,7 @@ type 'id move_location = (** Sorts *) -type sort_info = Pp.std_ppcmds option +type sort_info = string option type glob_sort = GProp | GSet | GType of sort_info (** Casts *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 7ed29ba39e..95709e6f7a 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -370,7 +370,11 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = let detype_sort = function | Prop Null -> GProp | Prop Pos -> GSet - | Type u -> GType (if !print_universes then Some (Univ.pr_uni u) else None) + | Type u -> + GType + (if !print_universes + then Some (Pp.string_of_ppcmds (Univ.pr_uni u)) + else None) type binder_kind = BProd | BLambda | BLetIn diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 38f5fc1c6d..0948b31f36 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -113,7 +113,7 @@ let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" let pr_glob_sort = function | GProp -> str "Prop" | GSet -> str "Set" - | GType u -> hov 0 (str "Type" ++ pr_opt (pr_in_comment (fun x->x)) u) + | GType u -> hov 0 (str "Type" ++ pr_opt (pr_in_comment str) u) let pr_id = pr_id let pr_name = pr_name |