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 /kernel/modops.ml | |
| 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 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 29 |
1 files changed, 15 insertions, 14 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 859f83e05..585b38a08 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -612,19 +612,20 @@ let clean_bounded_mod_expr sign = (** {6 Stm machinery } *) -let rec join_module mb = - implem_iter join_signature join_expression mb.mod_expr; - Option.iter join_expression mb.mod_type_alg; - join_signature mb.mod_type -and join_modtype mt = - Option.iter join_expression mt.typ_expr_alg; - join_signature mt.typ_expr -and join_field (l,body) = match body with - |SFBconst sb -> join_constant_body sb +let rec join_module otab mb = + implem_iter (join_signature otab) (join_expression otab) mb.mod_expr; + Option.iter (join_expression otab) mb.mod_type_alg; + join_signature otab mb.mod_type +and join_modtype otab mt = + Option.iter (join_expression otab) mt.typ_expr_alg; + join_signature otab mt.typ_expr +and join_field otab (l,body) = match body with + |SFBconst sb -> join_constant_body otab sb |SFBmind _ -> () - |SFBmodule m -> join_module m - |SFBmodtype m -> join_modtype m -and join_structure struc = List.iter join_field struc -and join_signature sign = functor_iter join_modtype join_structure sign -and join_expression me = functor_iter join_modtype (fun _ -> ()) me + |SFBmodule m -> join_module otab m + |SFBmodtype m -> join_modtype otab m +and join_structure otab struc = List.iter (join_field otab) struc +and join_signature otab sign = + functor_iter (join_modtype otab) (join_structure otab) sign +and join_expression otab me = functor_iter (join_modtype otab) (fun _ -> ()) me |