package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Ltac2_plugin.Tac2ffiSource

Ltac2 FFI
Sourcetype 'a repr
Sourceval repr_of : 'a repr -> 'a -> Tac2val.valexpr
Sourceval repr_to : 'a repr -> Tac2val.valexpr -> 'a
Sourceval make_repr : ('a -> Tac2val.valexpr) -> (Tac2val.valexpr -> 'a) -> 'a repr
Sourceval 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.

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

WARNING these functions copy

Sourceval to_string : Tac2val.valexpr -> string
Sourceval string : string repr
Sourceval of_list : ('a -> Tac2val.valexpr) -> 'a list -> Tac2val.valexpr
Sourceval to_list : (Tac2val.valexpr -> 'a) -> Tac2val.valexpr -> 'a list
Sourceval list : 'a repr -> 'a list repr
Sourceval of_constr : EConstr.t -> Tac2val.valexpr
Sourceval to_constr : Tac2val.valexpr -> EConstr.t
Sourceval constr : EConstr.t repr
Sourceval exninfo : Exninfo.info repr
Sourceval of_block : (int * Tac2val.valexpr array) -> Tac2val.valexpr
Sourceval to_block : Tac2val.valexpr -> int * Tac2val.valexpr array
Sourceval block : (int * Tac2val.valexpr array) repr
Sourceval of_array : ('a -> Tac2val.valexpr) -> 'a array -> Tac2val.valexpr
Sourceval to_array : (Tac2val.valexpr -> 'a) -> Tac2val.valexpr -> 'a array
Sourceval array : 'a repr -> 'a array repr
Sourceval of_tuple : Tac2val.valexpr array -> Tac2val.valexpr
Sourceval to_tuple : Tac2val.valexpr -> Tac2val.valexpr array
Sourceval of_pair : ('a -> Tac2val.valexpr) -> ('b -> Tac2val.valexpr) -> ('a * 'b) -> Tac2val.valexpr
Sourceval to_pair : (Tac2val.valexpr -> 'a) -> (Tac2val.valexpr -> 'b) -> Tac2val.valexpr -> 'a * 'b
Sourceval pair : 'a repr -> 'b repr -> ('a * 'b) repr
Sourceval of_triple : ('a -> Tac2val.valexpr) -> ('b -> Tac2val.valexpr) -> ('c -> Tac2val.valexpr) -> ('a * 'b * 'c) -> Tac2val.valexpr
Sourceval to_triple : (Tac2val.valexpr -> 'a) -> (Tac2val.valexpr -> 'b) -> (Tac2val.valexpr -> 'c) -> Tac2val.valexpr -> 'a * 'b * 'c
Sourceval triple : 'a repr -> 'b repr -> 'c repr -> ('a * 'b * 'c) repr
Sourceval of_option : ('a -> Tac2val.valexpr) -> 'a option -> Tac2val.valexpr
Sourceval to_option : (Tac2val.valexpr -> 'a) -> Tac2val.valexpr -> 'a option
Sourceval option : 'a repr -> 'a option repr
Sourceval of_evar : Evar.t -> Tac2val.valexpr
Sourceval to_evar : Tac2val.valexpr -> Evar.t
Sourceval evar : Evar.t repr
Sourceval pp : Pp.t repr
Sourceval reference : Names.GlobRef.t repr
Sourceval of_ext : 'a Tac2dyn.Val.tag -> 'a -> Tac2val.valexpr
Sourceval to_ext : 'a Tac2dyn.Val.tag -> Tac2val.valexpr -> 'a
Sourceval repr_ext : 'a Tac2dyn.Val.tag -> 'a repr
Sourceval open_ : (Names.KerName.t * Tac2val.valexpr array) repr
Sourceval of_uint63 : Uint63.t -> Tac2val.valexpr
Sourceval to_uint63 : Tac2val.valexpr -> Uint63.t
Sourceval uint63 : Uint63.t repr
Sourceval float : Float64.t repr
Sourceval of_pstring : Pstring.t -> Tac2val.valexpr
Sourceval to_pstring : Tac2val.valexpr -> Pstring.t
Sourceval pstring : Pstring.t repr
Sourcetype ('a, 'b) fun1
Sourceval app_fun1 : ('a, 'b) fun1 -> 'a repr -> 'b repr -> 'a -> 'b Proofview.tactic
Sourceval to_fun1 : 'a repr -> 'b repr -> Tac2val.valexpr -> ('a, 'b) fun1
Sourceval fun1 : 'a repr -> 'b repr -> ('a, 'b) fun1 repr
Dynamic tags
Sourceval val_transparent_state : TransparentState.t Tac2dyn.Val.tag

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

Exception

Sourceexception 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