diff options
| author | Matthieu Sozeau | 2015-10-28 11:16:47 -0400 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-28 12:38:09 -0400 |
| commit | 89be9efbf6dbd8a04fb8ccab4c9aa7a11b9a0f03 (patch) | |
| tree | 12f3f9e9e414b86098b935fdf73a61fcddeffb77 /printing/prettyp.ml | |
| parent | 908dcd613b12645f3b62bf44c2696b80a0b16940 (diff) | |
Printing of @{} instances for polymorphic references in Print and About.
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 14 |
1 files changed, 11 insertions, 3 deletions
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) |