diff options
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index f55bfb504f..a2bdb30773 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -583,11 +583,15 @@ let print_constant with_values sep sp udecl = str"*** [ " ++ print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ - Printer.pr_universes sigma univs ?priv:cb.const_private_poly_univs - | Some (c, ctx) -> + Printer.pr_universes sigma univs + | Some (c, priv, ctx) -> + let priv = match priv with + | Opaqueproof.PrivateMonomorphic () -> None + | Opaqueproof.PrivatePolymorphic (_, ctx) -> Some ctx + in 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_universes sigma univs ?priv:cb.const_private_poly_univs) + Printer.pr_universes sigma univs ?priv) let gallina_print_constant_with_infos sp udecl = print_constant true " = " sp udecl ++ @@ -723,7 +727,7 @@ let print_full_pure_context env sigma = | OpaqueDef lc -> str "Theorem " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++ - str "Proof " ++ pr_lconstr_env env sigma (Opaqueproof.force_proof Library.indirect_accessor (Global.opaque_tables ()) lc) + str "Proof " ++ pr_lconstr_env env sigma (fst (Opaqueproof.force_proof Library.indirect_accessor (Global.opaque_tables ()) lc)) | Def c -> str "Definition " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++ |