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/cooking.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/cooking.ml')
| -rw-r--r-- | kernel/cooking.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 5f6aebc4e..412742611 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -161,10 +161,10 @@ let on_body ml hy f = function OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f { Opaqueproof.modlist = ml; abstract = hy } o) -let constr_of_def = function +let constr_of_def otab = function | Undef _ -> assert false | Def cs -> Mod_subst.force_constr cs - | OpaqueDef lc -> Opaqueproof.force_proof lc + | OpaqueDef lc -> Opaqueproof.force_proof otab lc let expmod_constr_subst cache modlist subst c = let c = expmod_constr cache modlist c in @@ -189,7 +189,8 @@ let lift_univs cb subst = subst, Univ.UContext.make (inst,cstrs') else subst, cb.const_universes -let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } = +let cook_constant env { from = cb; info } = + let { Opaqueproof.modlist; abstract } = info in let cache = RefTable.create 13 in let abstract, usubst, abs_ctx = abstract in let usubst, univs = lift_univs cb usubst in @@ -211,7 +212,7 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } = | TemplateArity (ctx,s) -> let t = mkArity (ctx,Type s.template_level) in let typ = abstract_constant_type (expmod t) hyps in - let j = make_judge (constr_of_def body) typ in + let j = make_judge (constr_of_def (opaque_tables env) body) typ in Typeops.make_polymorphic_if_constant_for_ind env j in let projection pb = |