diff options
Diffstat (limited to 'kernel/term_typing.mli')
| -rw-r--r-- | kernel/term_typing.mli | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index ef01ece185..f82312245b 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -22,9 +22,7 @@ open Entries type 'a effect_handler = env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int) -type _ trust = -| Pure : unit trust -| SideEffects : 'a effect_handler -> 'a Entries.seff_wrap trust +type typing_context val translate_local_def : env -> Id.t -> section_def_entry -> constr * Sorts.relevance * types @@ -32,15 +30,17 @@ val translate_local_def : env -> Id.t -> section_def_entry -> val translate_local_assum : env -> types -> types * Sorts.relevance val translate_constant : - 'a trust -> env -> Constant.t -> 'a constant_entry -> - Opaqueproof.proofterm constant_body + env -> Constant.t -> 'a constant_entry -> + typing_context constant_body val translate_recipe : env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body +val check_delayed : 'a effect_handler -> typing_context -> 'a proof_output -> (Constr.t * Univ.ContextSet.t Opaqueproof.delayed_universes) + (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : trust:'a trust -> env -> - 'a constant_entry -> Opaqueproof.proofterm Cooking.result +val infer_declaration : env -> + 'a constant_entry -> typing_context Cooking.result val build_constant_declaration : env -> Opaqueproof.proofterm Cooking.result -> Opaqueproof.proofterm constant_body |