diff options
Diffstat (limited to 'kernel/term_typing.mli')
| -rw-r--r-- | kernel/term_typing.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 1fa5eca2e3..ef01ece185 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -24,7 +24,7 @@ type 'a effect_handler = type _ trust = | Pure : unit trust -| SideEffects : 'a effect_handler -> 'a trust +| SideEffects : 'a effect_handler -> 'a Entries.seff_wrap trust val translate_local_def : env -> Id.t -> section_def_entry -> constr * Sorts.relevance * types @@ -33,14 +33,14 @@ val translate_local_assum : env -> types -> types * Sorts.relevance val translate_constant : 'a trust -> env -> Constant.t -> 'a constant_entry -> - constant_body + Opaqueproof.proofterm constant_body -val translate_recipe : hcons:bool -> env -> Constant.t -> Cooking.recipe -> constant_body +val translate_recipe : env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body (** Internal functions, mentioned here for debug purpose only *) val infer_declaration : trust:'a trust -> env -> - 'a constant_entry -> Cooking.result + 'a constant_entry -> Opaqueproof.proofterm Cooking.result val build_constant_declaration : - Constant.t -> env -> Cooking.result -> constant_body + env -> Opaqueproof.proofterm Cooking.result -> Opaqueproof.proofterm constant_body |