diff options
| author | Maxime Dénès | 2018-09-03 12:41:46 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-03 12:41:46 +0200 |
| commit | da58ae4c620412923ea84b1982e8765f6be145a8 (patch) | |
| tree | 8518269959c007a7c70bdbd80a968ebff03c6415 /kernel/safe_typing.mli | |
| parent | 3bc0c82700a805e889198b810cc0148f6479cbe1 (diff) | |
| parent | 568f3b69d407f7b5a47d1fdd6ca2bbf3edb5be72 (diff) | |
Merge PR #7912: Simplify effects API
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 17 |
1 files changed, 4 insertions, 13 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index aca77ccd13..502e2970a1 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -41,29 +41,20 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment (** {6 Stm machinery } *) -type private_constant type private_constants -type private_constant_role = - | Subproof - | Schema of inductive * string - val side_effects_of_private_constants : - private_constants -> Entries.side_effect list + private_constants -> Entries.side_eff list (** Return the list of individual side-effects in the order of their creation. *) val empty_private_constants : private_constants -val add_private : private_constant -> private_constants -> private_constants -(** Add a constant to a list of private constants. The former must be more - recent than all constants appearing in the latter, i.e. one should not - create a dependency cycle. *) val concat_private : private_constants -> private_constants -> private_constants (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in [e1] must be more recent than those of [e2]. *) -val private_con_of_con : safe_environment -> Constant.t -> private_constant -val private_con_of_scheme : kind:string -> safe_environment -> (inductive * Constant.t) list -> private_constant +val private_con_of_con : safe_environment -> Constant.t -> private_constants +val private_con_of_scheme : kind:string -> safe_environment -> (inductive * Constant.t) list -> private_constants val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output val inline_private_constants_in_constr : @@ -105,7 +96,7 @@ type global_declaration = | GlobalRecipe of Cooking.recipe type exported_private_constant = - Constant.t * private_constant_role + Constant.t * Entries.side_effect_role val export_private_constants : in_section:bool -> private_constants Entries.definition_entry -> |