diff options
| author | Pierre-Marie Pédrot | 2019-06-04 13:44:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-17 15:20:02 +0200 |
| commit | 5316d205993bb3fe3f69e8984fe53d4d50aa8d2a (patch) | |
| tree | 8016562d06949b981a3e58e71103b02aea7f1c44 /printing | |
| parent | 7e47fea5ce050c8129ba2d6f94e93fbc29763a3b (diff) | |
Allow to delay polymorphic opaque constants.
We had to move the private opaque constraints out of the constant declaration
into the opaque table. The API is not very pretty yet due to a pervasive
confusion between monomorphic global constraints and polymorphic local ones,
but once we get rid of futures in the kernel this should be magically solved.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/prettyp.ml | 12 | ||||
| -rw-r--r-- | printing/printmod.ml | 2 |
2 files changed, 9 insertions, 5 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index f55bfb504f..396c954b42 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -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 " := " ++ diff --git a/printing/printmod.ml b/printing/printmod.ml index bd97104f60..52a3616152 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -297,7 +297,7 @@ let print_body is_impl extent env mp (l,body) = hov 2 (str ":= " ++ Printer.pr_lconstr_env env sigma (Mod_subst.force_constr l)) | _ -> mt ()) ++ str "." ++ - Printer.pr_abstract_universe_ctx sigma ctx ?priv:cb.const_private_poly_univs) + Printer.pr_abstract_universe_ctx sigma ctx) | SFBmind mib -> match extent with | WithContents -> |