diff options
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 18 |
1 files changed, 5 insertions, 13 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 4078a909..502e2970 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 -> @@ -221,6 +212,7 @@ val delta_of_senv : open Retroknowledge val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a +[@@ocaml.deprecated "Use the projection of Environ.env"] val register : field -> Retroknowledge.entry -> Constr.constr -> safe_transformer0 |