diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-16 00:05:03 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-26 15:12:10 +0200 |
| commit | ce830b204ad52f8b3655d2cb4672662120d83101 (patch) | |
| tree | 988e160ecf888787c6d005b08db0cdfd62935460 /kernel/term_typing.ml | |
| parent | 3fcf0930874d7200f2503ac7084b1d6669d59540 (diff) | |
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.
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 |