diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-20 20:33:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-20 20:33:27 +0100 |
| commit | 12c61c7ab522ea58bf8c5692de7130e124a2cc0a (patch) | |
| tree | 6a58fba73892d1f300c058326ff069e938fccf10 /kernel/term_typing.ml | |
| parent | 579770c44251f2b8d01ecc6252810ec80da374f5 (diff) | |
Exporting the function handling side-effects only applied to terms.
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 5c95aacae..dce30413d 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -286,7 +286,7 @@ let translate_local_def env id centry = let translate_mind env kn mie = Indtypes.check_inductive env kn mie -let handle_side_effects env ce = { ce with +let handle_entry_side_effects env ce = { ce with const_entry_body = Future.chain ~greedy:true ~pure:true ce.const_entry_body (fun ((body, ctx), side_eff) -> (handle_side_effects env body side_eff, ctx), Declareops.no_seff); |