diff options
| author | Pierre-Marie Pédrot | 2019-05-13 00:26:56 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-15 00:20:40 +0200 |
| commit | 3cdaffab75414f3f59386a4b76c6b00c94bc8b0e (patch) | |
| tree | 822d2dee865ba8801592f153223bb5ad0bd38aa4 /kernel/safe_typing.mli | |
| parent | e74fce3090323b4d3734f84ee8cf6dc1f5e85953 (diff) | |
Simplify the private constant API.
We ungroup the rewrite scheme-defined constants, while only exporting a
function to turn the last added constant into a private constant.
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 6fcdef9a10..d6c7022cf5 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -48,8 +48,8 @@ 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_constants -val private_con_of_scheme : kind:string -> safe_environment -> (inductive * Constant.t) list -> private_constants +val private_constant : safe_environment -> Entries.side_effect_role -> Constant.t -> private_constants +(** Constant must be the last definition of the safe_environment. *) val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output val inline_private_constants_in_constr : |