diff options
| author | Pierre-Marie Pédrot | 2019-06-05 10:35:17 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-11 16:59:07 +0200 |
| commit | e753855167e5629775b604128c6efc9d58ee626c (patch) | |
| tree | 7abdebb08679b76a80cf9d1a36f05b91a538c223 /kernel/safe_typing.mli | |
| parent | 3d162ca9095ff9299be5cc8847636a36b8e49f1e (diff) | |
Remove the side-effect role from the kernel.
We move the role data into the evarmap instead.
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 |