package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Ltac_plugin.TacenvSource

This module centralizes the various ways of registering tactics.

Tactic naming
Sourceval locate_extended_all_tactic : Libnames.qualid -> Tacexpr.ltac_constant list
Sourceval exists_tactic : Libnames.full_path -> bool
Sourceval shortest_qualid_of_tactic : Tacexpr.ltac_constant -> Libnames.qualid
Tactic notations

Type of tactic alias, used in the TacAlias node.

Sourcetype 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

Sourceval register_alias : alias -> alias_tactic -> unit

Register a tactic alias.

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

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

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 = {
  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

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

Low-level access to all Ltac entries currently defined.

ML tactic extensions

Type of external tactics, used by TacML.

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

Register an external tactic.

Sourceval 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