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 (5)

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.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

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 import_type : Libnames.qualid -> Names.Id.t -> 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
Sourcetype notation_target = Libnames.qualid option * int option
Sourceval pr_register_notation : Tac2expr.sexpr list -> notation_target -> Tac2expr.raw_tacexpr -> Pp.t
Sourceval pr_register_abbreviation : Names.Id.t CAst.t -> Tac2expr.raw_tacexpr -> Pp.t
Sourceval register_notation_interpretation : notation_interpretation_data -> unit
Sourceval register_custom_entry : Names.lident -> unit
Sourceval perform_eval : pstate:Declare.Proof.t option -> Tac2expr.raw_tacexpr -> unit
Notations
Sourcetype syntax_class_rule =
  1. | SyntaxRule : (Tac2expr.raw_tacexpr, _, 'a) Procq.Symbol.t * ('a -> Tac2expr.raw_tacexpr) -> syntax_class_rule
Sourcetype used_levels
Sourceval no_used_levels : used_levels
Sourceval union_used_levels : used_levels -> used_levels -> used_levels
Sourcetype 'glb syntax_class_decl = {
  1. intern_synclass : Tac2expr.sexpr list -> used_levels * 'glb;
  2. interp_synclass : 'glb -> syntax_class_rule;
}
Sourceval register_syntax_class : Names.Id.t -> _ syntax_class_decl -> unit

Create a new syntax class with the provided name

Sourcetype syntax_class
Sourceval intern_syntax_class : Tac2expr.sexpr -> used_levels * syntax_class

Use this to internalize the syntax class arguments for interpretation functions

Sourceval interp_syntax_class : syntax_class -> syntax_class_rule

Use this to interpret the syntax class arguments 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
module Tac2Custom : module type of Names.KerName

Common APIs on name tables.

Sourceval find_custom_entry : Tac2Custom.t -> Tac2expr.raw_tacexpr Procq.Entry.t

NB: Do not save the result of this function across summary resets, the Entry.t gets regenerated on (parsing) summary unfreeze.

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

Evaluate a tactic expression in the current environment

Parsing entries
Sourcemodule Pltac : sig ... end