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/prettyp.ml | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

(limited to 'printing/prettyp.ml')

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index b8c5fd4cfc..7e625af0de 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -73,7 +73,11 @@ let print_ref reduce ref =
       in it_mkProd_or_LetIn ccl ctx
     else typ in
   let univs = Global.universes_of_global ref in
-  hov 0 (pr_global ref ++ str " :" ++ spc () ++ pr_ltype typ ++ 
+  let inst =
+    if Global.is_polymorphic ref then Printer.pr_universe_instance univs
+    else mt ()
+  in
+  hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype typ ++ 
   	   Printer.pr_universe_ctx univs)
 
 (********************************)
@@ -473,6 +477,10 @@ let print_typed_body (val_0,typ) =
 let ungeneralized_type_of_constant_type t = 
   Typeops.type_of_constant_type (Global.env ()) t
 
+let print_instance cb =
+  if cb.const_polymorphic then pr_universe_instance cb.const_universes
+  else mt()
+				
 let print_constant with_values sep sp =
   let cb = Global.lookup_constant sp in
   let val_0 = Global.body_of_constant_body cb in
@@ -485,11 +493,11 @@ let print_constant with_values sep sp =
     match val_0 with
     | None ->
 	str"*** [ " ++
-	print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++
+	print_basename sp ++ print_instance cb ++ str " : " ++ cut () ++ pr_ltype typ ++
 	str" ]" ++
 	Printer.pr_universe_ctx univs
     | _ ->
-	print_basename sp ++ str sep ++ cut () ++
+	print_basename sp ++ print_instance cb ++ str sep ++ cut () ++
 	(if with_values then print_typed_body (val_0,typ) else pr_ltype typ)++
         Printer.pr_universe_ctx univs)
 
-- 
cgit v1.2.3


From 0132b5b51fc1856356fb74130d3dea7fd378f76c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 28 Oct 2015 12:36:20 -0400
Subject: Univs: local names handling.

Keep user-side information on the names used in instances of universe
polymorphic references and use them for printing.
---
 printing/prettyp.ml | 38 ++++++++++++++++++++++++--------------
 1 file changed, 24 insertions(+), 14 deletions(-)

(limited to 'printing/prettyp.ml')

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 7e625af0de..84649e6ebf 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -73,12 +73,15 @@ let print_ref reduce ref =
       in it_mkProd_or_LetIn ccl ctx
     else typ in
   let univs = Global.universes_of_global ref in
+  let env = Global.env () in
+  let bl = Universes.universe_binders_of_global ref in
+  let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
   let inst =
-    if Global.is_polymorphic ref then Printer.pr_universe_instance univs
+    if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs
     else mt ()
   in
-  hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype typ ++ 
-  	   Printer.pr_universe_ctx univs)
+  hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype_env env sigma typ ++ 
+  	   Printer.pr_universe_ctx sigma univs)
 
 (********************************)
 (** Printing implicit arguments *)
@@ -467,18 +470,19 @@ let gallina_print_section_variable id =
   print_named_decl id ++
   with_line_skip (print_name_infos (VarRef id))
 
-let print_body = function
-  | Some c  -> pr_lconstr c
+let print_body env evd = function
+  | Some c  -> pr_lconstr_env env evd c
   | None -> (str"<no body>")
 
-let print_typed_body (val_0,typ) =
-  (print_body val_0 ++ fnl () ++ str "     : " ++ pr_ltype typ)
+let print_typed_body env evd (val_0,typ) =
+  (print_body env evd val_0 ++ fnl () ++ str "     : " ++ pr_ltype_env env evd typ)
 
 let ungeneralized_type_of_constant_type t = 
   Typeops.type_of_constant_type (Global.env ()) t
 
-let print_instance cb =
-  if cb.const_polymorphic then pr_universe_instance cb.const_universes
+let print_instance sigma cb =
+  if cb.const_polymorphic then
+    pr_universe_instance sigma cb.const_universes
   else mt()
 				
 let print_constant with_values sep sp =
@@ -489,17 +493,23 @@ let print_constant with_values sep sp =
   let univs = Univ.instantiate_univ_context 
     (Global.universes_of_constant_body cb)
   in
+  let ctx =
+    Evd.evar_universe_context_of_binders
+      (Universes.universe_binders_of_global (ConstRef sp))
+  in
+  let env = Global.env () and sigma = Evd.from_ctx ctx in
+  let pr_ltype = pr_ltype_env env sigma in
   hov 0 (pr_polymorphic cb.const_polymorphic ++
     match val_0 with
     | None ->
 	str"*** [ " ++
-	print_basename sp ++ print_instance cb ++ str " : " ++ cut () ++ pr_ltype typ ++
+	print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++
 	str" ]" ++
-	Printer.pr_universe_ctx univs
+	Printer.pr_universe_ctx sigma univs
     | _ ->
-	print_basename sp ++ print_instance cb ++ str sep ++ cut () ++
-	(if with_values then print_typed_body (val_0,typ) else pr_ltype typ)++
-        Printer.pr_universe_ctx univs)
+	print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++
+	(if with_values then print_typed_body env sigma (val_0,typ) else pr_ltype typ)++
+        Printer.pr_universe_ctx sigma univs)
 
 let gallina_print_constant_with_infos sp =
   print_constant true " = " sp ++
-- 
cgit v1.2.3