diff options
| author | Emilio Jesus Gallego Arias | 2020-05-20 00:47:21 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-26 14:38:10 +0200 |
| commit | d83e95cce852c5471593a27d0fdca39a262c885f (patch) | |
| tree | 9117298b6f6d0a69e6863578858de27ddb23e8ba /vernac/declare.mli | |
| parent | 7d183d8a12a03a608a3dc8a724142468b45886ac (diff) | |
[declare] [api] Removal of deprecated functions
The previous refactoring in `Declare` to add `CInfo.t` makes this a
good moment to clean overlays up w.r.t. deprecation.
All cases but one is just a matter of simple renaming, for the other
the use of an internal API is replaced by newer API.
Diffstat (limited to 'vernac/declare.mli')
| -rw-r--r-- | vernac/declare.mli | 17 |
1 files changed, 1 insertions, 16 deletions
diff --git a/vernac/declare.mli b/vernac/declare.mli index 6f104e764d..002328b63f 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -280,7 +280,7 @@ val fixpoint_message : int array option -> Id.t list -> unit val check_exists : Id.t -> unit -(** {6 For legacy support, do not use} *) +(** {6 For internal support, do not use} *) module Internal : sig @@ -337,21 +337,6 @@ val get_current_goal_context : Proof.t -> Evd.evar_map * Environ.env environment and empty evar_map. *) val get_current_context : Proof.t -> Evd.evar_map * Environ.env -(** XXX: Temporarily re-exported for 3rd party code; don't use *) -val build_constant_by_tactic : - name:Names.Id.t -> - ?opaque:opacity_flag -> - uctx:UState.t -> - sign:Environ.named_context_val -> - poly:bool -> - EConstr.types -> - unit Proofview.tactic -> - Evd.side_effects proof_entry * bool * UState.t -[@@ocaml.deprecated "This function is deprecated, used newer API in declare"] - -val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit -[@@ocaml.deprecated "Use DeclareUctx.declare_universe_context"] - type locality = Locality.locality = Discharge | Global of import_status (** Information for a constant *) |