package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
Toplevel definitions
val register_ltac : ?deprecation:Deprecation.t -> ?local:bool -> ?mut:bool -> Tac2expr.rec_flag -> (Names.lname * Tac2expr.raw_tacexpr) list -> unit
val register_type : ?local:bool -> Tac2expr.rec_flag -> (Libnames.qualid * Tac2expr.redef_flag * Tac2expr.raw_quant_typedef) list -> unit
val register_primitive : ?deprecation:Deprecation.t -> ?local:bool -> Names.lident -> Tac2expr.raw_typexpr -> Tac2expr.ml_tactic_name -> unit
val register_struct : Attributes.vernac_flags -> Tac2expr.strexpr -> unit
val register_notation : ?deprecation:Deprecation.t -> ?local:bool -> Tac2expr.sexpr list -> int option -> Tac2expr.raw_tacexpr -> unit
val perform_eval : pstate:Declare.Proof.t option -> Tac2expr.raw_tacexpr -> unit
Notations
type scope_rule =
  1. | ScopeRule : (Tac2expr.raw_tacexpr, _, 'a) Pcoq.Symbol.t * ('a -> Tac2expr.raw_tacexpr) -> scope_rule
type scope_interpretation = Tac2expr.sexpr list -> scope_rule
val register_scope : Names.Id.t -> scope_interpretation -> unit

Create a new scope with the provided name

val parse_scope : Tac2expr.sexpr -> scope_rule

Use this to interpret the subscopes for interpretation functions

Inspecting
val print_ltac : Libnames.qualid -> unit
Eval loop
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
Parsing entries
module Pltac : sig ... end
Hooks
val register_constr_quotations : (unit -> unit) Hook.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct