diff options
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 1ce790ebbb..b2f6668577 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -73,12 +73,13 @@ val is_joined_environment : safe_environment -> bool (** Insertion of global axioms or definitions *) -type 'a effect_entry = -| EffectEntry : private_constants Entries.seff_wrap effect_entry -| PureEntry : unit effect_entry - type global_declaration = - | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration +| ConstantEntry : Entries.constant_entry -> global_declaration +| OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declaration + +type side_effect_declaration = +| DefinitionEff : Entries.definition_entry -> side_effect_declaration +| OpaqueEff : Constr.constr Entries.opaque_entry -> side_effect_declaration type exported_private_constant = Constant.t @@ -86,10 +87,13 @@ val export_private_constants : private_constants Entries.proof_output -> (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer -(** returns the main constant plus a certificate of its validity *) +(** returns the main constant *) val add_constant : - side_effect:'a effect_entry -> Label.t -> global_declaration -> - (Constant.t * 'a) safe_transformer + Label.t -> global_declaration -> Constant.t safe_transformer + +(** Similar to add_constant but also returns a certificate *) +val add_private_constant : + Label.t -> side_effect_declaration -> (Constant.t * private_constants) safe_transformer (** Adding an inductive type *) |