diff options
| -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]. |