From 63c7aa195022a908e0ee43d3cfb48c836405a835 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 9 Jan 2019 13:30:04 +0100
Subject: Stop [Print] from saying [is (not) universe polymorphic].

[About] still says it.

Close #9056.
---
 printing/prettyp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing/prettyp.ml')

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index c417ef8a66..408bd5f60b 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -267,7 +267,6 @@ let print_name_infos ref =
        print_ref true ref None; blankline]
     else
       [] in
-  print_polymorphism ref @
   print_type_in_type ref @
   print_primitive ref @
   type_info_for_implicit @
@@ -838,6 +837,7 @@ let print_about_any ?loc env sigma k udecl =
     Dumpglob.add_glob ?loc ref;
       pr_infos_list
        (print_ref false ref udecl :: blankline ::
+        print_polymorphism ref @
 	print_name_infos ref @
 	(if Pp.ismt rb then [] else [rb]) @
 	print_opacity ref @
-- 
cgit v1.2.3