diff options
Diffstat (limited to 'tactics/tacenv.mli')
| -rw-r--r-- | tactics/tacenv.mli | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli index 29677fd4..2df6bb04 100644 --- a/tactics/tacenv.mli +++ b/tactics/tacenv.mli @@ -23,6 +23,9 @@ val register_alias : alias -> glob_tactic_expr -> unit val interp_alias : alias -> glob_tactic_expr (** Recover the the body of an alias. Raises an anomaly if it does not exist. *) +val check_alias : alias -> bool +(** Returns [true] if an alias is defined, false otherwise. *) + (** {5 Coq tactic definitions} *) val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit @@ -41,6 +44,19 @@ val interp_ltac : KerName.t -> glob_tactic_expr (** Find a user-defined tactic by name. Raise [Not_found] if it is absent. *) val is_ltac_for_ml_tactic : KerName.t -> bool +(** Whether the tactic is defined from ML-side *) + +type ltac_entry = { + tac_for_ml : bool; + (** Whether the tactic is defined from ML-side *) + tac_body : glob_tactic_expr; + (** The current body of the tactic *) + tac_redef : ModPath.t list; + (** List of modules redefining the tactic in reverse chronological order *) +} + +val ltac_entries : unit -> ltac_entry KNmap.t +(** Low-level access to all Ltac entries currently defined. *) (** {5 ML tactic extensions} *) |