package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

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

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2

doc/ltac2_plugin/Ltac2_plugin/Tac2entries/index.html

Module Ltac2_plugin.Tac2entriesSource

Toplevel definitions
Sourceval register_ltac : ?deprecation:Deprecation.t -> ?local:bool -> ?mut:bool -> Tac2expr.rec_flag -> (Names.lname * Tac2expr.raw_tacexpr) list -> unit
Sourceval register_type : ?local:bool -> ?abstract:bool -> Tac2expr.rec_flag -> (Libnames.qualid * Tac2expr.redef_flag * Tac2expr.raw_quant_typedef) list -> unit
Sourceval register_primitive : ?deprecation:Deprecation.t -> ?local:bool -> Names.lident -> Tac2expr.raw_typexpr -> Tac2expr.ml_tactic_name -> unit
Sourceval register_struct : Attributes.vernac_flags -> Tac2expr.strexpr -> unit
Sourcetype notation_interpretation_data
Sourceval register_notation_interpretation : notation_interpretation_data -> unit
Sourceval perform_eval : pstate:Declare.Proof.t option -> Tac2expr.raw_tacexpr -> unit
Notations
Sourcetype scope_rule =
  1. | ScopeRule : (Tac2expr.raw_tacexpr, _, 'a) Pcoq.Symbol.t * ('a -> Tac2expr.raw_tacexpr) -> scope_rule
Sourcetype scope_interpretation = Tac2expr.sexpr list -> scope_rule
Sourceval register_scope : Names.Id.t -> scope_interpretation -> unit

Create a new scope with the provided name

Sourceval parse_scope : Tac2expr.sexpr -> scope_rule

Use this to interpret the subscopes for interpretation functions

Inspecting
Sourceval print_located_tactic : Libnames.qualid -> unit

Display the absolute name of a tactic.

Sourceval print_ltac2 : Libnames.qualid -> unit

Display the definition of a tactic.

Sourceval print_ltac2_type : Libnames.qualid -> unit

Display the definition of a type.

Sourceval print_signatures : unit -> unit

Print types of all definitions in scope.

Sourceval typecheck_expr : Tac2expr.raw_tacexpr -> unit
Sourceval globalize_expr : Tac2expr.raw_tacexpr -> unit
Eval loop
Sourceval call : pstate:Declare.Proof.t -> Goal_select.t option -> with_end_tac:bool -> Tac2expr.raw_tacexpr -> Declare.Proof.t

Evaluate a tactic expression in the current environment

Sourceval call_par : pstate:Declare.Proof.t -> with_end_tac:bool -> Tac2expr.raw_tacexpr -> Declare.Proof.t
Parsing entries
Sourcemodule Pltac : sig ... end