diff options
| author | Gaëtan Gilbert | 2020-01-30 23:34:49 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-30 23:34:49 +0100 |
| commit | a7af2f6571d007b6f83a1ec9252b52f69907a965 (patch) | |
| tree | 014747da5aa139b93c3c6d3e015499bbfb525541 /kernel/safe_typing.mli | |
| parent | 92a294ca53752b61b0270a719826ffc759a25e8d (diff) | |
export_private_constants doesn't use the [constr in_univ_ctx] argument
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 92bbd264fa..c879481c66 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -84,8 +84,8 @@ type side_effect_declaration = type exported_private_constant = Constant.t val export_private_constants : - private_constants Entries.proof_output -> - (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer + private_constants -> + exported_private_constant list safe_transformer (** returns the main constant *) val add_constant : |