package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (6)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.3.0.tar.gz
sha256=3f0fc283e8644394aa9c7a6e3995b6d9ebbe1e6dda712bf431f9c372dcef95ad

doc/ltac_plugin/Ltac_plugin/Tacenv/index.html

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;
  4. alias_is_ml : Tacexpr.ml_tactic_entry 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.

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

Replace a Ltac with the given name and body.

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.KerName.Map.t

Low-level access to all Ltac entries currently defined.

ML tactic extensions
module TacStore : Store.S
Sourcetype interp_sign = {
  1. lfun : Geninterp.Val.t Names.Id.Map.t;
  2. poly : PolyFlags.t;
  3. extra : TacStore.t;
}
Sourcetype ml_tactic = Geninterp.Val.t list -> interp_sign -> unit Proofview.tactic

Type of external tactics, used by TacML.

Sourceval register_ml_tactic : ?overwrite:bool -> ?warn:(?loc:Loc.t -> unit -> unit) -> Tacexpr.ml_tactic_name -> ml_tactic array -> unit

Register an external tactic.

Sourceval intern_check_ml_tac_alias : ?loc:Loc.t -> Tacexpr.ml_tactic_entry -> unit
Sourceval interp_ml_tactic : Tacexpr.ml_tactic_entry -> ml_tactic

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