package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

This module centralizes the various ways of registering tactics.

Tactic naming
val locate_tactic : Libnames.qualid -> Tacexpr.ltac_constant
val locate_extended_all_tactic : Libnames.qualid -> Tacexpr.ltac_constant list
val exists_tactic : Libnames.full_path -> bool
val shortest_qualid_of_tactic : Tacexpr.ltac_constant -> Libnames.qualid
Tactic notations
type alias = Names.KerName.t

Type of tactic alias, used in the TacAlias node.

type alias_tactic = {
  1. alias_args : Names.Id.t list;
  2. alias_body : Tacexpr.glob_tactic_expr;
  3. alias_deprecation : Deprecation.t option;
}

Contents of a tactic notation

val register_alias : alias -> alias_tactic -> unit

Register a tactic alias.

val interp_alias : alias -> alias_tactic

Recover 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.

Coq tactic definitions
val register_ltac : bool -> bool -> ?deprecation:Deprecation.t -> Names.Id.t -> Tacexpr.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 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.

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.

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

val is_ltac_for_ml_tactic : Names.KerName.t -> bool

Whether the tactic is defined from ML-side

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

The tactic deprecation notice, if any

type ltac_entry = {
  1. tac_for_ml : bool;
    (*

    Whether the tactic is defined from ML-side

    *)
  2. tac_body : Tacexpr.glob_tactic_expr;
    (*

    The current body of the tactic

    *)
  3. tac_redef : Names.ModPath.t list;
    (*

    List of modules redefining the tactic in reverse chronological order

    *)
  4. tac_deprecation : Deprecation.t option;
    (*

    Deprecation notice to be printed when the tactic is used

    *)
}
val ltac_entries : unit -> ltac_entry Names.KNmap.t

Low-level access to all Ltac entries currently defined.

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

Type of external tactics, used by TacML.

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

Register an external tactic.

val interp_ml_tactic : Tacexpr.ml_tactic_entry -> ml_tactic

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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct