From 89be9efbf6dbd8a04fb8ccab4c9aa7a11b9a0f03 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 28 Oct 2015 11:16:47 -0400
Subject: Printing of @{} instances for polymorphic references in Print and
 About.

---
 printing/printmod.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'printing/printmod.ml')

diff --git a/printing/printmod.ml b/printing/printmod.ml
index 53d0508c7f..8031de27d4 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -94,8 +94,12 @@ let print_one_inductive env mib ((_,i) as ind) =
   let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in
   let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
   let envpar = push_rel_context params env in
+  let inst =
+    if mib.mind_polymorphic then Printer.pr_universe_instance mib.mind_universes
+    else mt ()
+  in
   hov 0 (
-    pr_id mip.mind_typename ++ brk(1,4) ++ print_params env Evd.empty params ++
+    pr_id mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env Evd.empty params ++
     str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ str " :=") ++
   brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes
 
-- 
cgit v1.2.3