diff options
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index f2920a90ee..50f6832ffa 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_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 *) @@ -87,18 +87,16 @@ type 'a effect_entry = type global_declaration = | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration -type exported_private_constant = - Constant.t * Entries.side_effect_role +type exported_private_constant = Constant.t val export_private_constants : in_section:bool -> private_constants Entries.proof_output -> (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer -(** returns the main constant plus a list of auxiliary constants (empty - unless one requires the side effects to be exported) *) +(** returns the main constant plus a certificate of its validity *) val add_constant : - ?role:Entries.side_effect_role -> in_section:bool -> Label.t -> global_declaration -> - (Constant.t * private_constants) safe_transformer + side_effect:'a effect_entry -> in_section:bool -> Label.t -> global_declaration -> + (Constant.t * 'a) safe_transformer val add_recipe : in_section:bool -> Label.t -> Cooking.recipe -> Constant.t safe_transformer |