diff options
| author | Maxime Dénès | 2017-12-20 00:38:47 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-20 00:38:47 +0100 |
| commit | b3b3798fca7fd05f31cb921f981c15ee81507b0d (patch) | |
| tree | 21e626fe84012dac3043bd89b4ed20ac81b89742 /kernel/term_typing.ml | |
| parent | 7fac7294a1906a8df835e6d7be5bb1bca3f727b5 (diff) | |
| parent | 25f09e86ba1a3ab3c24d5e17336b01315a205e00 (diff) | |
Merge PR #6449: Let definitions must not contain side-effects when reaching the kernel.
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 70dd6438d4..761eab511a 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -533,14 +533,10 @@ type side_effect_role = type exported_side_effect = Constant.t * constant_body * side_effect_role -let export_side_effects mb env ce = - match ce with - | ParameterEntry e -> [], ParameterEntry e - | ProjectionEntry e -> [], ProjectionEntry e - | DefinitionEntry c -> +let export_side_effects mb env c = let { const_entry_body = body } = c in let _, eff = Future.force body in - let ce = DefinitionEntry { c with + let ce = { c with const_entry_body = Future.chain body (fun (b_ctx, _) -> b_ctx, ()) } in let not_exists (c,_,_,_) = @@ -609,9 +605,9 @@ let translate_recipe env kn r = let hcons = DirPath.is_empty dir in build_constant_declaration kn env (Cooking.cook_constant ~hcons env r) -let translate_local_def mb env id centry = +let translate_local_def env id centry = let open Cooking in - let decl = infer_declaration ~trust:mb env None (DefinitionEntry centry) in + let decl = infer_declaration ~trust:Pure env None (DefinitionEntry centry) in let typ = decl.cook_type in if Option.is_empty decl.cook_context && !Flags.record_aux_file then begin match decl.cook_body with |