diff options
| author | Enrico Tassi | 2014-10-08 10:33:20 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-10-13 18:13:20 +0200 |
| commit | 9d0011125da2b24ccf006154ab205c6987fb03d2 (patch) | |
| tree | fb28bab986b15fb05e9d9ddbf0556f0a62f29b54 /printing | |
| parent | e62984e17cad223448feddeccac0d40e1f604c31 (diff) | |
library/opaqueTables: enable their use in interactive mode
Before this patch opaque tables were only growing, making them unusable
in interactive mode (leak on Undo).
With this patch the opaque tables are functional and part of the env.
I.e. a constant_body can point to the proof term in 2 ways:
1) directly (before the constant is discharged)
2) indirectly, via an int, that is mapped by the opaque table to
the proof term.
This is now consistent in batch/interactive mode
This is step 0 to make an interactive coqtop able to dump a .vo/.vi
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 e0f6ef25cc..efdbb0dc42 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -470,10 +470,10 @@ let ungeneralized_type_of_constant_type t = let print_constant with_values sep sp = let cb = Global.lookup_constant sp in - let val_0 = Declareops.body_of_constant cb in + let val_0 = Global.body_of_constant_body cb in let typ = Declareops.type_of_constant cb in let typ = ungeneralized_type_of_constant_type typ in - let univs = Univ.instantiate_univ_context (Declareops.universes_of_constant cb) in + let univs = Univ.instantiate_univ_context (Global.universes_of_constant_body cb) in hov 0 (pr_polymorphic cb.const_polymorphic ++ match val_0 with | None -> @@ -626,7 +626,7 @@ let print_full_pure_context () = | OpaqueDef lc -> str "Theorem " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++ - str "Proof " ++ pr_lconstr (Opaqueproof.force_proof lc) + str "Proof " ++ pr_lconstr (Opaqueproof.force_proof (Global.opaque_tables ()) lc) | Def c -> str "Definition " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype typ ++ cut () ++ str " := " ++ |