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/ltac2_plugin/Ltac2_plugin/Tac2syn/index.html

Module Ltac2_plugin.Tac2synSource

module Tac2Scope : module type of Names.KerName

Common APIs on name tables.

Sourceval declare_scope : Names.Id.t -> unit
Sourceval open_scope : Libobject.locality -> Libnames.qualid -> unit
Sourceval close_scope : Libobject.locality -> Libnames.qualid -> unit
Sourceval default_scope : unit -> Tac2Scope.t
Sourceval current_scopes : unit -> Tac2Scope.t list
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.

Sourcemodule Syntax : sig ... end
Sourcetype syntax_class_rule =
  1. | SyntaxRule : 'a Syntax.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

Sourcetype notation_data =
  1. | UntypedNota of Tac2expr.raw_tacexpr
  2. | TypedNota of {
    1. nota_prms : int;
    2. nota_argtys : int Tac2expr.glb_typexpr Names.Id.Map.t;
    3. nota_ty : int Tac2expr.glb_typexpr;
    4. nota_body : Tac2expr.glb_tacexpr;
    }
Sourceval interp_notation : ?loc:Loc.t -> Tac2Scope.t list -> Tac2expr.tacsyn -> notation_data * (Names.lname * Tac2expr.raw_tacexpr) list
Sourcetype ('scope, 'body) notation_interpretation
Sourceval ltac2_notation_cat : Libobject.category
Sourcetype notation_target = {
  1. target_entry : Libnames.qualid option;
  2. target_level : int option;
  3. target_scope : Libnames.qualid option;
}
Sourceval pr_register_notation : Tac2expr.sexpr list -> notation_target -> Tac2expr.raw_tacexpr -> Pp.t
Sourceval register_notation : Attributes.vernac_flags -> Tac2expr.sexpr list -> notation_target -> 'body -> (Libnames.qualid option, 'body) notation_interpretation

Does not handle the deprecated abbreviation syntax

Sourceval intern_notation_interpretation : (Names.Id.Set.t -> 'raw -> 'glb) -> (Libnames.qualid option, 'raw) notation_interpretation -> (Tac2Scope.t, 'glb) notation_interpretation
Sourceval register_notation_interpretation : (Tac2Scope.t, notation_data) notation_interpretation -> unit
Sourceval register_custom_entry : Names.lident -> unit
Sourcemodule Internal : sig ... end