diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-02-24 20:46:32 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-02-26 14:53:08 +0100 |
| commit | 15b6c9b6fa268a9af6dd4f05961e469545e92a6f (patch) | |
| tree | 2e5aacf72993b448d1e80b0cbfbf0a09091ecb32 /kernel/cooking.ml | |
| parent | e6556db92d4c4fe9ba38f26b89f805095d2b2638 (diff) | |
Lazyconstr -> Opaqueproof
Make this module deal only with opaque proofs.
Make discharging/substitution invariant more explicit via a third constructor.
Diffstat (limited to 'kernel/cooking.ml')
| -rw-r--r-- | kernel/cooking.ml | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 75642648d..f81bcceb3 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -109,7 +109,7 @@ let abstract_constant_type = let abstract_constant_body = List.fold_left (fun c d -> mkNamedLambda_or_LetIn d c) -type recipe = { from : constant_body; info : Lazyconstr.cooking_info } +type recipe = { from : constant_body; info : Opaqueproof.cooking_info } type inline = bool type result = @@ -118,21 +118,22 @@ type result = let on_body ml hy f = function | Undef _ as x -> x - | Def cs -> Def (Lazyconstr.from_val (f (Lazyconstr.force cs))) - | OpaqueDef lc -> - OpaqueDef (Lazyconstr.discharge_direct_lazy_constr ml hy f lc) + | Def cs -> Def (Mod_subst.from_val (f (Mod_subst.force_constr cs))) + | OpaqueDef o -> + OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f + { Opaqueproof.modlist = ml; abstract = hy } o) let constr_of_def = function | Undef _ -> assert false - | Def cs -> Lazyconstr.force cs - | OpaqueDef lc -> Lazyconstr.force_opaque lc + | Def cs -> Mod_subst.force_constr cs + | OpaqueDef lc -> Opaqueproof.force_proof lc -let cook_constr { Lazyconstr.modlist ; abstract } c = +let cook_constr { Opaqueproof.modlist ; abstract } c = let cache = Hashtbl.create 13 in let hyps = Context.map_named_context (expmod_constr cache modlist) abstract in abstract_constant_body (expmod_constr cache modlist c) hyps -let cook_constant env { from = cb; info = { Lazyconstr.modlist; abstract } } = +let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } = let cache = Hashtbl.create 13 in let hyps = Context.map_named_context (expmod_constr cache modlist) abstract in let body = on_body modlist hyps |