diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-10-29 15:39:20 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-10-29 15:39:20 +0100 |
| commit | dd1998f1a9bc2aae2e83aa4e349318d2466b6aea (patch) | |
| tree | 6cedfaa501e65fa22011430f09f1a7d37ece50d2 /kernel/term_typing.mli | |
| parent | 78378ba9a79b18a658828d7a110414ad18b9a732 (diff) | |
Cleanup API and comments of 908dcd613
Diffstat (limited to 'kernel/term_typing.mli')
| -rw-r--r-- | kernel/term_typing.mli | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 509160ccc..2e6aa161b 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -19,30 +19,34 @@ val translate_local_assum : env -> types -> types val mk_pure_proof : constr -> side_effects proof_output -val handle_side_effects : env -> constr -> side_effects -> constr +val inline_side_effects : env -> constr -> side_effects -> constr (** Returns the term where side effects have been turned into let-ins or beta redexes. *) -val handle_entry_side_effects : env -> side_effects definition_entry -> side_effects definition_entry -(** Same as {!handle_side_effects} but applied to entries. Only modifies the +val inline_entry_side_effects : + env -> side_effects definition_entry -> side_effects definition_entry +(** Same as {!inline_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 uniq_seff : side_effects -> side_effects -val translate_constant : structure_body -> env -> constant -> side_effects constant_entry -> constant_body +val translate_constant : + structure_body -> env -> constant -> side_effects constant_entry -> + constant_body -(* Checks weather the side effects in constant_entry can be trusted. - * Returns the list of effects to be exported. - * Note: It forces the Future.computation. *) type side_effect_role = | Subproof | Schema of inductive * string type exported_side_effect = - constant * constant_body * side_effects Entries.constant_entry * side_effect_role + constant * constant_body * side_effects constant_entry * side_effect_role -val validate_side_effects_for_export : +(* Given a constant entry containing side effects it exports them (either + * by re-checking them or trusting them). Returns the constant bodies to + * be pushed in the safe_env by safe typing. The main constant entry + * needs to be translated as usual after this step. *) +val export_side_effects : structure_body -> env -> side_effects constant_entry -> exported_side_effect list * side_effects constant_entry |