diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term_typing.ml | 2 | ||||
| -rw-r--r-- | kernel/term_typing.mli | 12 |
2 files changed, 9 insertions, 5 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 5c95aacae7..dce30413d9 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); diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 8be1c76e06..a699bce38d 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -20,10 +20,14 @@ val translate_local_assum : env -> types -> types val mk_pure_proof : constr -> proof_output -(* returns the same definition_entry but with side effects turned into - * let-ins or beta redexes. it is meant to get a term out of a not yet - * type checked proof *) -val handle_side_effects : env -> definition_entry -> definition_entry +val handle_side_effects : env -> constr -> Declareops.side_effects -> constr +(** Returns the term where side effects have been turned into let-ins or beta + redexes. *) + +val handle_entry_side_effects : env -> definition_entry -> definition_entry +(** Same as {!handle_side_effects} but applied to entries. Only modifies the + {!Entries.const_entry_body} field. It is meant to get a term out of a not + yet type checked proof. *) val translate_constant : env -> constant -> constant_entry -> constant_body |