diff options
| author | Emilio Jesus Gallego Arias | 2020-04-18 23:07:36 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-21 08:39:13 +0200 |
| commit | 77fc6ad50fb2bd95d19ecaee36fa34c7931a2bc1 (patch) | |
| tree | 7ed7bccbf1308dd814afe4be3258b4942d6f5ce6 | |
| parent | e04377e2c5eca2b47bd5f8db320069aa47040488 (diff) | |
[declare] Remove `declare_private_constant` from the public API.
This is an internal function for scheme declaration handled properly
now, we can also remove `pure_definition_entry` which is IMO good too.
| -rw-r--r-- | vernac/declare.mli | 18 |
1 files changed, 0 insertions, 18 deletions
diff --git a/vernac/declare.mli b/vernac/declare.mli index 73e0d7cd04..a551c621c4 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -160,16 +160,6 @@ val definition_entry -> constr -> Evd.side_effects proof_entry -(** XXX: Scheduled for removal from public API, use `DeclareDef` instead *) -val pure_definition_entry - : ?fix_exn:Future.fix_exn - -> ?opaque:bool - -> ?inline:bool - -> ?types:types - -> ?univs:Entries.universes_entry - -> constr - -> unit proof_entry - type import_status = ImportDefaultBehavior | ImportNeedQualified (** [declare_constant id cd] declares a global declaration @@ -187,14 +177,6 @@ val declare_constant -> Evd.side_effects constant_entry -> Constant.t -val declare_private_constant - : ?role:Evd.side_effect_role - -> ?local:import_status - -> name:Id.t - -> kind:Decls.logical_kind - -> unit proof_entry - -> Constant.t * Evd.side_effects - (** [inline_private_constants ~sideff ~uctx env ce] will inline the constants in [ce]'s body and return the body plus the updated [UState.t]. |