package coq-core

  1. Overview
  2. Docs
package coq-core
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 -> ?abstract: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
type notation_interpretation_data
val register_notation_interpretation : notation_interpretation_data -> 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_located_tactic : Libnames.qualid -> unit

Display the absolute name of a tactic.

val print_ltac2 : Libnames.qualid -> unit

Display the definition of a tactic.

val print_ltac2_type : Libnames.qualid -> unit

Display the definition of a type.

val print_signatures : unit -> unit

Print types of all definitions in scope.

val typecheck_expr : Tac2expr.raw_tacexpr -> unit
val globalize_expr : Tac2expr.raw_tacexpr -> unit
Eval loop
val 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

val call_par : pstate:Declare.Proof.t -> with_end_tac:bool -> Tac2expr.raw_tacexpr -> Declare.Proof.t
Parsing entries
module Pltac : sig ... end
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