From 6869b22e2546b69acb74e18dc491029897ba36a3 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Mon, 28 Apr 2014 13:44:42 +0200
Subject: Print universes in module printing

---
 printing/printmod.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'printing/printmod.ml')

diff --git a/printing/printmod.ml b/printing/printmod.ml
index 8d05e2d6d..b7be2c0f5 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -153,8 +153,8 @@ let print_body is_impl env mp (l,body) =
 		spc () ++
 		hov 2 (str ":= " ++
 		       Printer.pr_lconstr_env env (Mod_subst.force_constr l))
-	      | _ -> mt ()) ++
-            str ".")
+	      | _ -> mt ()) ++ str "." ++
+	    Printer.pr_universe_ctx cb.const_universes)
     | SFBmind mib ->
       try
 	let env = Option.get env in
-- 
cgit v1.2.3