diff options
| author | Enrico Tassi | 2019-06-12 07:09:01 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-12 07:09:01 +0200 |
| commit | 0d4300771e4a6a26d948872262a79695a38c7e0d (patch) | |
| tree | ab31353a6f01b17270f87d5d0670fc5085c75130 /kernel/safe_typing.mli | |
| parent | 3d162ca9095ff9299be5cc8847636a36b8e49f1e (diff) | |
| parent | ee270f7d111e5e71e90a4f3eb5e4edf5c13ea7e3 (diff) | |
Merge PR #10334: Remove the side-effect role from the kernel.
Reviewed-by: gares
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 770caf5406..3e902303c3 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -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 |