diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-08 10:33:20 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-13 18:13:20 +0200 |
| commit | 9d0011125da2b24ccf006154ab205c6987fb03d2 (patch) | |
| tree | fb28bab986b15fb05e9d9ddbf0556f0a62f29b54 /toplevel | |
| 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 'toplevel')
| -rw-r--r-- | toplevel/vernac.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 248a6b513..dcce58199 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -321,7 +321,7 @@ let compile verbosely f = Stm.join (); let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); - Library.save_library_to ldir long_f_dot_v; + Library.save_library_to ldir long_f_dot_v (Global.opaque_tables ()); Aux_file.record_in_aux_at Loc.ghost "vo_compile_time" (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); Aux_file.stop_aux_file (); @@ -333,7 +333,8 @@ let compile verbosely f = let _ = load_vernac verbosely long_f_dot_v in Stm.finish (); check_pending_proofs (); - Library.save_library_to ~todo:Stm.dump ldir long_f_dot_v + Library.save_library_to ~todo:Stm.dump_final ldir long_f_dot_v + (Global.opaque_tables ()) | Vi2Vo -> let open Filename in let open Library in |