From ce830b204ad52f8b3655d2cb4672662120d83101 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 16 Jul 2017 00:05:03 +0200 Subject: Further simplication: do not recreate entries for side-effects. This is actually useless, the code does not depend on the value of the entry for side-effects. --- kernel/term_typing.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 03bd8426f..23c5b6f58 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -544,7 +544,7 @@ type side_effect_role = | Schema of inductive * string type exported_side_effect = - constant * constant_body * unit constant_entry * side_effect_role + constant * constant_body * side_effect_role let export_side_effects mb env ce = match ce with @@ -596,7 +596,7 @@ let export_side_effects mb env ce = List.fold_left (fun (env,cbs) (kn, ocb, u, r) -> let ce = constant_entry_of_side_effect ocb u in let cb = translate_constant Pure env kn ce in - (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs)) + (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,r) :: cbs)) (env,[]) cbs in translate_seff sl rest (cbs @ acc) env | Some sl, cbs :: rest -> @@ -604,7 +604,7 @@ let export_side_effects mb env ce = let cbs = List.map turn_direct cbs in let env = List.fold_left push_seff env cbs in let ecbs = List.map (fun (kn,cb,u,r) -> - kn, cb, constant_entry_of_side_effect cb u, r) cbs in + kn, cb, r) cbs in translate_seff (Some (sl-cbs_len)) rest (ecbs @ acc) env in translate_seff trusted seff [] env -- cgit v1.2.3