diff options
| author | Pierre-Marie Pédrot | 2019-05-21 19:22:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-24 09:00:10 +0200 |
| commit | d3c931cd8c84d1b7d9d5763e20221d51700f0709 (patch) | |
| tree | 58ca99c4f6007bc66294c41354bb68bf9d71044b /printing | |
| parent | 2fa3dc389a58ca4a390b99995d82e6c089add163 (diff) | |
Remove the indirect opaque accessor hooks from Opaqueproof.
We simply pass them as arguments, now that they are not called by the
kernel anymore.
The checker definitely needs to access the opaque proofs. In order not to
touch the API at all, I added a hook there, but it could also be provided
as an additional argument, at the cost of changing all the upwards callers.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/prettyp.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 9541ea5882..fca33a24bf 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -549,7 +549,7 @@ let print_instance sigma cb = let print_constant with_values sep sp udecl = let cb = Global.lookup_constant sp in - let val_0 = Global.body_of_constant_body cb in + let val_0 = Global.body_of_constant_body Library.indirect_accessor cb in let typ = cb.const_type in let univs = let open Univ in @@ -557,7 +557,7 @@ let print_constant with_values sep sp udecl = match cb.const_body with | Undef _ | Def _ | Primitive _ -> cb.const_universes | OpaqueDef o -> - let body_uctxs = Opaqueproof.force_constraints otab o in + let body_uctxs = Opaqueproof.force_constraints Library.indirect_accessor otab o in match cb.const_universes with | Monomorphic ctx -> Monomorphic (ContextSet.union body_uctxs ctx) @@ -717,7 +717,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 (Global.opaque_tables ()) lc) + str "Proof " ++ pr_lconstr_env env sigma (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 " := " ++ |