diff options
| author | Pierre-Marie Pédrot | 2016-05-13 19:38:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-18 18:54:43 +0200 |
| commit | 806e3bc0ecfbf0a6bfd20e80caa8250e60d39152 (patch) | |
| tree | 21bda11bb7526d8dccc8c3883245ecf02762fc74 /printing/prettyp.ml | |
| parent | 575da16f72ac125ba7e50b1bfe63302dee639973 (diff) | |
Print the type-in-type flag in various user-facing functions.
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 9745a79250..ad67becd01 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -215,6 +215,12 @@ let print_polymorphism ref = else "not universe polymorphic") ] else [] +let print_type_in_type ref = + let unsafe = Global.is_type_in_type ref in + if unsafe then + [ pr_global ref ++ str " relies on an unsafe universe hierarchy"] + else [] + let print_primitive_record recflag mipv = function | Some (Some (_, ps,_)) -> let eta = match recflag with @@ -244,6 +250,7 @@ let print_name_infos ref = else [] in print_polymorphism ref @ + print_type_in_type ref @ print_primitive ref @ type_info_for_implicit @ print_renames_list (mt()) renames @ |