diff options
| author | Matthieu Sozeau | 2018-11-27 11:20:57 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-11-27 11:20:57 +0100 |
| commit | f6a2d21b6c2a93cb70fde235fc897fb75ea51384 (patch) | |
| tree | 8913811d7ff06686a0ec837296545cae12007f85 /printing/prettyp.ml | |
| parent | dddb72b2f45f39f04e91aa9099bcd1064c629504 (diff) | |
| parent | c58ea20fba5a5ce54aaf62182dfd3ee8a368d529 (diff) | |
Merge PR #8850: Private universes for opaque polymorphic constants.
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 712eb21ee6..f9f4d7f7f8 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -96,8 +96,9 @@ let print_ref reduce ref udecl = then Printer.pr_universe_instance sigma inst else mt () in + let priv = None in (* We deliberately don't print private univs in About. *) hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ - Printer.pr_abstract_universe_ctx sigma ?variance univs) + Printer.pr_abstract_universe_ctx sigma ?variance univs ~priv) (********************************) (** Printing implicit arguments *) @@ -580,11 +581,11 @@ let print_constant with_values sep sp udecl = str"*** [ " ++ print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ - Printer.pr_constant_universes sigma univs + Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs | Some (c, ctx) -> print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++ (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ - Printer.pr_constant_universes sigma univs) + Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs) let gallina_print_constant_with_infos sp udecl = print_constant true " = " sp udecl ++ |