diff options
| author | Maxime Dénès | 2019-10-23 10:01:20 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-10-23 10:01:20 +0200 |
| commit | a88dec59499afa7fbe01e4bd0e8400aebd5ffbcf (patch) | |
| tree | b2d64405d7fbfde84ada7ec7012260be1dd3c51c /kernel/safe_typing.mli | |
| parent | 1f25366ac049dad2f4fa255f47acf84c3ccb4b02 (diff) | |
| parent | 593e784250eca0f38479109395a5fbc605f2c3c4 (diff) | |
Merge PR #10884: Last stop before CEP 40
Reviewed-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: gares
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 *) |