From 806e3bc0ecfbf0a6bfd20e80caa8250e60d39152 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 13 May 2016 19:38:13 +0200
Subject: Print the type-in-type flag in various user-facing functions.

---
 printing/prettyp.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'printing/prettyp.ml')

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