Module `Ltac_plugin.Tacenv`Source

This module centralizes the various ways of registering tactics.

Tactic naming

val push_tactic : 
  Nametab.visibility ->
  Libnames.full_path ->
  Tacexpr.ltac_constant ->
  unit

Sourceval locate_tactic : Libnames.qualid -> Tacexpr.ltac_constant

Sourceval locate_extended_all_tactic : Libnames.qualid -> Tacexpr.ltac_constant list

Sourceval exists_tactic : Libnames.full_path -> bool

Sourceval path_of_tactic : Tacexpr.ltac_constant -> Libnames.full_path

Sourceval shortest_qualid_of_tactic : Tacexpr.ltac_constant -> Libnames.qualid

Tactic notations

Sourcetype alias = Names.KerName.t

Type of tactic alias, used in the TacAlias node.

Sourcetype alias_tactic = {

alias_args : Names.Id.t list;
alias_body : Tacexpr.glob_tactic_expr;
alias_deprecation : Deprecation.t option;

}

Contents of a tactic notation

Sourceval register_alias : alias -> alias_tactic -> unit

Sourceval interp_alias : alias -> alias_tactic

Recover the body of an alias. Raises an anomaly if it does not exist.

Sourceval check_alias : alias -> bool

Returns true if an alias is defined, false otherwise.

Coq tactic definitions

Source

val register_ltac : 
  bool ->
  bool ->
  ?deprecation:Deprecation.t ->
  Names.Id.t ->
  Tacexpr.glob_tactic_expr ->
  unit

The first boolean indicates whether this is done from ML side, rather than Coq side. If the second boolean flag is set to true, then this is a local definition. It also puts the Ltac name in the nametab, so that it can be used unqualified.

Source

val redefine_ltac : 
  bool ->
  ?deprecation:Deprecation.t ->
  Names.KerName.t ->
  Tacexpr.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.

Sourceval interp_ltac : Names.KerName.t -> Tacexpr.glob_tactic_expr

Find a user-defined tactic by name. Raise Not_found if it is absent.

Sourceval is_ltac_for_ml_tactic : Names.KerName.t -> bool

Whether the tactic is defined from ML-side

Sourceval tac_deprecation : Names.KerName.t -> Deprecation.t option

The tactic deprecation notice, if any

Sourcetype ltac_entry = {

tac_for_ml : bool;
(*
Whether the tactic is defined from ML-side
*)
tac_body : Tacexpr.glob_tactic_expr;
(*
The current body of the tactic
*)
tac_redef : Names.ModPath.t list;
(*
List of modules redefining the tactic in reverse chronological order
*)
tac_deprecation : Deprecation.t option;
(*
Deprecation notice to be printed when the tactic is used
*)

}

Sourceval ltac_entries : unit -> ltac_entry Names.KNmap.t

Low-level access to all Ltac entries currently defined.

ML tactic extensions

Source

type ml_tactic =
  Geninterp.Val.t list ->
  Geninterp.interp_sign ->
  unit Proofview.tactic

Type of external tactics, used by TacML.

Source

val register_ml_tactic : 
  ?overwrite:bool ->
  Tacexpr.ml_tactic_name ->
  ml_tactic array ->
  unit

Sourceval interp_ml_tactic : Tacexpr.ml_tactic_entry -> ml_tactic

Get the named tactic. Raises a user error if it does not exist.

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac_plugin/Ltac_plugin/Tacenv/index.html

Module `Ltac_plugin.Tacenv`Source

Tactic naming

Tactic notations

Coq tactic definitions

ML tactic extensions

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac_plugin/Ltac_plugin/Tacenv/index.html

Module Ltac_plugin.TacenvSource

Tactic naming

Tactic notations

Coq tactic definitions

ML tactic extensions

Module `Ltac_plugin.Tacenv`Source