diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /plugins/ltac/tacenv.mli | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'plugins/ltac/tacenv.mli')
-rw-r--r-- | plugins/ltac/tacenv.mli | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli index e0bac67d..d5d36c97 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -12,6 +12,7 @@ open Names open Libnames open Tacexpr open Geninterp +open Vernacinterp (** This module centralizes the various ways of registering tactics. *) @@ -29,7 +30,11 @@ val shortest_qualid_of_tactic : ltac_constant -> qualid type alias = KerName.t (** Type of tactic alias, used in the [TacAlias] node. *) -type alias_tactic = Id.t list * glob_tactic_expr +type alias_tactic = + { alias_args: Id.t list; + alias_body: glob_tactic_expr; + alias_deprecation: Vernacinterp.deprecation option; + } (** Contents of a tactic notation *) val register_alias : alias -> alias_tactic -> unit @@ -43,7 +48,8 @@ val check_alias : alias -> bool (** {5 Coq tactic definitions} *) -val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit +val register_ltac : bool -> bool -> ?deprecation:deprecation -> Id.t -> + glob_tactic_expr -> unit (** Register a new Ltac with the given name and body. The first boolean indicates whether this is done from ML side, rather than @@ -51,7 +57,8 @@ val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit definition. It also puts the Ltac name in the nametab, so that it can be used unqualified. *) -val redefine_ltac : bool -> KerName.t -> glob_tactic_expr -> unit +val redefine_ltac : bool -> ?deprecation:deprecation -> KerName.t -> + glob_tactic_expr -> unit (** Replace a Ltac with the given name and body. If the boolean flag is set to true, then this is a local redefinition. *) @@ -61,6 +68,9 @@ val interp_ltac : KerName.t -> glob_tactic_expr val is_ltac_for_ml_tactic : KerName.t -> bool (** Whether the tactic is defined from ML-side *) +val tac_deprecation : KerName.t -> deprecation option +(** The tactic deprecation notice, if any *) + type ltac_entry = { tac_for_ml : bool; (** Whether the tactic is defined from ML-side *) @@ -68,6 +78,8 @@ type ltac_entry = { (** The current body of the tactic *) tac_redef : ModPath.t list; (** List of modules redefining the tactic in reverse chronological order *) + tac_deprecation : deprecation option; + (** Deprecation notice to be printed when the tactic is used *) } val ltac_entries : unit -> ltac_entry KNmap.t |