package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

T

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

Maintainers

C

coqdev@inria.fr

Sources

coq-8.14.1.tar.gz

sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3

doc/ltac2_plugin/Ltac2_plugin/Tac2entries/index.html

Module `Ltac2_plugin.Tac2entries`Source

Toplevel definitions

Source

val register_ltac : 
  ?deprecation:Deprecation.t ->
  ?local:bool ->
  ?mut:bool ->
  Tac2expr.rec_flag ->
  (Names.lname * Tac2expr.raw_tacexpr) list ->
  unit

Source

val register_type : 
  ?local:bool ->
  Tac2expr.rec_flag ->
  (Libnames.qualid * Tac2expr.redef_flag * Tac2expr.raw_quant_typedef) list ->
  unit

Source

val register_primitive : 
  ?deprecation:Deprecation.t ->
  ?local:bool ->
  Names.lident ->
  Tac2expr.raw_typexpr ->
  Tac2expr.ml_tactic_name ->
  unit

Source

val register_struct : 
  ?deprecation:Deprecation.t ->
  ?local:bool ->
  Tac2expr.strexpr ->
  unit

Source

val register_notation : 
  ?deprecation:Deprecation.t ->
  ?local:bool ->
  Tac2expr.sexpr list ->
  int option ->
  Tac2expr.raw_tacexpr ->
  unit

Source

val perform_eval : 
  pstate:Declare.Proof.t option ->
  Tac2expr.raw_tacexpr ->
  unit

Notations

Sourcetype scope_rule =

| 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_ltac : Libnames.qualid -> unit

Eval loop

Source

val call : 
  pstate:Declare.Proof.t ->
  with_end_tac:bool ->
  Tac2expr.raw_tacexpr ->
  Declare.Proof.t

Evaluate a tactic expression in the current environment

Toplevel exceptions

Sourceval backtrace : Tac2expr.backtrace Exninfo.t

Parsing entries

Sourcemodule Pltac : sig ... end

Hooks

Sourceval register_constr_quotations : (unit -> unit) Hook.t

On This Page

Toplevel definitions
Notations
Inspecting
Eval loop
Toplevel exceptions
Parsing entries
Hooks

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac2_plugin/Ltac2_plugin/Tac2entries/index.html

Module Ltac2_plugin.Tac2entriesSource

Toplevel definitions

Notations

Inspecting

Eval loop

Toplevel exceptions

Parsing entries

Hooks

Module `Ltac2_plugin.Tac2entries`Source