package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
Ltac2 FFI
type 'a repr
val repr_of : 'a repr -> 'a -> Tac2val.valexpr
val repr_to : 'a repr -> Tac2val.valexpr -> 'a
val make_repr : ('a -> Tac2val.valexpr) -> (Tac2val.valexpr -> 'a) -> 'a repr
val map_repr : ('a -> 'b) -> ('b -> 'a) -> 'a repr -> 'b repr

These functions allow to convert back and forth between OCaml and Ltac2 data representation. The to_* functions raise an anomaly whenever the data has not expected shape.

val of_unit : unit -> Tac2val.valexpr
val to_unit : Tac2val.valexpr -> unit
val unit : unit repr
val of_int : int -> Tac2val.valexpr
val to_int : Tac2val.valexpr -> int
val int : int repr
val of_bool : bool -> Tac2val.valexpr
val to_bool : Tac2val.valexpr -> bool
val bool : bool repr
val of_char : char -> Tac2val.valexpr
val to_char : Tac2val.valexpr -> char
val char : char repr
val of_bytes : Bytes.t -> Tac2val.valexpr
val to_bytes : Tac2val.valexpr -> Bytes.t
val bytes : Bytes.t repr
val of_string : string -> Tac2val.valexpr

WARNING these functions copy

val to_string : Tac2val.valexpr -> string
val string : string repr
val of_list : ('a -> Tac2val.valexpr) -> 'a list -> Tac2val.valexpr
val to_list : (Tac2val.valexpr -> 'a) -> Tac2val.valexpr -> 'a list
val list : 'a repr -> 'a list repr
val of_constr : EConstr.t -> Tac2val.valexpr
val to_constr : Tac2val.valexpr -> EConstr.t
val constr : EConstr.t repr
val err : Exninfo.iexn repr
val exn : Exninfo.iexn repr
val of_exninfo : Exninfo.info -> Tac2val.valexpr
val to_exninfo : Tac2val.valexpr -> Exninfo.info
val exninfo : Exninfo.info repr
val of_ident : Names.Id.t -> Tac2val.valexpr
val to_ident : Tac2val.valexpr -> Names.Id.t
val ident : Names.Id.t repr
val of_closure : Tac2val.closure -> Tac2val.valexpr
val to_closure : Tac2val.valexpr -> Tac2val.closure
val closure : Tac2val.closure repr
val of_block : (int * Tac2val.valexpr array) -> Tac2val.valexpr
val to_block : Tac2val.valexpr -> int * Tac2val.valexpr array
val block : (int * Tac2val.valexpr array) repr
val of_array : ('a -> Tac2val.valexpr) -> 'a array -> Tac2val.valexpr
val to_array : (Tac2val.valexpr -> 'a) -> Tac2val.valexpr -> 'a array
val array : 'a repr -> 'a array repr
val of_tuple : Tac2val.valexpr array -> Tac2val.valexpr
val to_tuple : Tac2val.valexpr -> Tac2val.valexpr array
val of_pair : ('a -> Tac2val.valexpr) -> ('b -> Tac2val.valexpr) -> ('a * 'b) -> Tac2val.valexpr
val to_pair : (Tac2val.valexpr -> 'a) -> (Tac2val.valexpr -> 'b) -> Tac2val.valexpr -> 'a * 'b
val pair : 'a repr -> 'b repr -> ('a * 'b) repr
val of_triple : ('a -> Tac2val.valexpr) -> ('b -> Tac2val.valexpr) -> ('c -> Tac2val.valexpr) -> ('a * 'b * 'c) -> Tac2val.valexpr
val to_triple : (Tac2val.valexpr -> 'a) -> (Tac2val.valexpr -> 'b) -> (Tac2val.valexpr -> 'c) -> Tac2val.valexpr -> 'a * 'b * 'c
val triple : 'a repr -> 'b repr -> 'c repr -> ('a * 'b * 'c) repr
val of_option : ('a -> Tac2val.valexpr) -> 'a option -> Tac2val.valexpr
val to_option : (Tac2val.valexpr -> 'a) -> Tac2val.valexpr -> 'a option
val option : 'a repr -> 'a option repr
val of_evar : Evar.t -> Tac2val.valexpr
val to_evar : Tac2val.valexpr -> Evar.t
val evar : Evar.t repr
val of_pp : Pp.t -> Tac2val.valexpr
val to_pp : Tac2val.valexpr -> Pp.t
val pp : Pp.t repr
val of_constant : Names.Constant.t -> Tac2val.valexpr
val to_constant : Tac2val.valexpr -> Names.Constant.t
val constant : Names.Constant.t repr
val instance : EConstr.EInstance.t repr
val of_reference : Names.GlobRef.t -> Tac2val.valexpr
val to_reference : Tac2val.valexpr -> Names.GlobRef.t
val reference : Names.GlobRef.t repr
val of_ext : 'a Tac2dyn.Val.tag -> 'a -> Tac2val.valexpr
val to_ext : 'a Tac2dyn.Val.tag -> Tac2val.valexpr -> 'a
val repr_ext : 'a Tac2dyn.Val.tag -> 'a repr
val open_ : (Names.KerName.t * Tac2val.valexpr array) repr
val of_uint63 : Uint63.t -> Tac2val.valexpr
val to_uint63 : Tac2val.valexpr -> Uint63.t
val uint63 : Uint63.t repr
val of_float : Float64.t -> Tac2val.valexpr
val to_float : Tac2val.valexpr -> Float64.t
val float : Float64.t repr
val of_pstring : Pstring.t -> Tac2val.valexpr
val to_pstring : Tac2val.valexpr -> Pstring.t
val pstring : Pstring.t repr
type ('a, 'b) fun1
val app_fun1 : ('a, 'b) fun1 -> 'a repr -> 'b repr -> 'a -> 'b Proofview.tactic
val to_fun1 : 'a repr -> 'b repr -> Tac2val.valexpr -> ('a, 'b) fun1
val fun1 : 'a repr -> 'b repr -> ('a, 'b) fun1 repr
val valexpr : Tac2val.valexpr repr
Dynamic tags
val val_constr : EConstr.t Tac2dyn.Val.tag
val val_ident : Names.Id.t Tac2dyn.Val.tag
val val_matching_context : Constr_matching.context Tac2dyn.Val.tag
val val_evar : Evar.t Tac2dyn.Val.tag
val val_pp : Pp.t Tac2dyn.Val.tag
val val_inductive : Names.inductive Tac2dyn.Val.tag
val val_constructor : Names.constructor Tac2dyn.Val.tag
val val_projection : Names.Projection.t Tac2dyn.Val.tag
val val_uint63 : Uint63.t Tac2dyn.Val.tag
val val_float : Float64.t Tac2dyn.Val.tag
val val_transparent_state : TransparentState.t Tac2dyn.Val.tag
val val_exninfo : Exninfo.info Tac2dyn.Val.tag

Toplevel representation of OCaml exceptions. Invariant: no LtacError should be put into a value with tag val_exn.

Exception

exception LtacError of Names.KerName.t * Tac2val.valexpr array

Ltac2-defined exceptions seen from OCaml side

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