Module `Ltac2_plugin.Tac2ffi`Source

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 of_preterm : Ltac_pretype.closed_glob_constr -> Tac2val.valexpr

Sourceval to_preterm : Tac2val.valexpr -> Ltac_pretype.closed_glob_constr

Sourceval preterm : Ltac_pretype.closed_glob_constr repr

Sourceval of_cast : Constr.cast_kind -> Tac2val.valexpr

Sourceval to_cast : Tac2val.valexpr -> Constr.cast_kind

Sourceval cast : Constr.cast_kind repr

Sourceval of_err : Exninfo.iexn -> Tac2val.valexpr

Sourceval to_err : Tac2val.valexpr -> Exninfo.iexn

Sourceval err : Exninfo.iexn repr

Sourceval of_exn : Exninfo.iexn -> Tac2val.valexpr

Sourceval to_exn : Tac2val.valexpr -> Exninfo.iexn

Sourceval exn : Exninfo.iexn repr

Sourceval of_exninfo : Exninfo.info -> Tac2val.valexpr

Sourceval to_exninfo : Tac2val.valexpr -> Exninfo.info

Sourceval exninfo : Exninfo.info repr

Sourceval of_ident : Names.Id.t -> Tac2val.valexpr

Sourceval to_ident : Tac2val.valexpr -> Names.Id.t

Sourceval ident : Names.Id.t repr

Sourceval of_closure : Tac2val.closure -> Tac2val.valexpr

Sourceval to_closure : Tac2val.valexpr -> Tac2val.closure

Sourceval closure : Tac2val.closure 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

Source

val of_pair : 
  ('a -> Tac2val.valexpr) ->
  ('b -> Tac2val.valexpr) ->
  ('a * 'b) ->
  Tac2val.valexpr

Source

val to_pair : 
  (Tac2val.valexpr -> 'a) ->
  (Tac2val.valexpr -> 'b) ->
  Tac2val.valexpr ->
  'a * 'b

Sourceval pair : 'a repr -> 'b repr -> ('a * 'b) repr

Source

val of_triple : 
  ('a -> Tac2val.valexpr) ->
  ('b -> Tac2val.valexpr) ->
  ('c -> Tac2val.valexpr) ->
  ('a * 'b * 'c) ->
  Tac2val.valexpr

Source

val 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_pattern : Pattern.constr_pattern -> Tac2val.valexpr

Sourceval to_pattern : Tac2val.valexpr -> Pattern.constr_pattern

Sourceval pattern : Pattern.constr_pattern repr

Sourceval of_evar : Evar.t -> Tac2val.valexpr

Sourceval to_evar : Tac2val.valexpr -> Evar.t

Sourceval evar : Evar.t repr

Sourceval of_pp : Pp.t -> Tac2val.valexpr

Sourceval to_pp : Tac2val.valexpr -> Pp.t

Sourceval pp : Pp.t repr

Sourceval of_constant : Names.Constant.t -> Tac2val.valexpr

Sourceval to_constant : Tac2val.valexpr -> Names.Constant.t

Sourceval constant : Names.Constant.t repr

Sourceval of_instance : EConstr.EInstance.t -> Tac2val.valexpr

Sourceval to_instance : Tac2val.valexpr -> EConstr.EInstance.t

Sourceval instance : EConstr.EInstance.t repr

Sourceval of_reference : Names.GlobRef.t -> Tac2val.valexpr

Sourceval to_reference : Tac2val.valexpr -> Names.GlobRef.t

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 of_open : (Names.KerName.t * Tac2val.valexpr array) -> Tac2val.valexpr

Sourceval to_open : Tac2val.valexpr -> Names.KerName.t * Tac2val.valexpr array

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 of_float : Float64.t -> Tac2val.valexpr

Sourceval to_float : Tac2val.valexpr -> Float64.t

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

Sourceval valexpr : Tac2val.valexpr repr

Dynamic tags

Sourceval val_constr : EConstr.t Tac2dyn.Val.tag

Sourceval val_ident : Names.Id.t Tac2dyn.Val.tag

Sourceval val_pattern : Pattern.constr_pattern Tac2dyn.Val.tag

Sourceval val_preterm : Ltac_pretype.closed_glob_constr Tac2dyn.Val.tag

Sourceval val_matching_context : Constr_matching.context Tac2dyn.Val.tag

Sourceval val_evar : Evar.t Tac2dyn.Val.tag

Sourceval val_pp : Pp.t Tac2dyn.Val.tag

Sourceval val_sort : EConstr.ESorts.t Tac2dyn.Val.tag

Sourceval val_cast : Constr.cast_kind Tac2dyn.Val.tag

Sourceval val_inductive : Names.inductive Tac2dyn.Val.tag

Sourceval val_constant : Names.Constant.t Tac2dyn.Val.tag

Sourceval val_constructor : Names.constructor Tac2dyn.Val.tag

Sourceval val_projection : Names.Projection.t Tac2dyn.Val.tag

Sourceval val_qvar : Sorts.QVar.t Tac2dyn.Val.tag

Sourceval val_case : Constr.case_info Tac2dyn.Val.tag

Source

val val_binder : 
  (Names.Name.t EConstr.binder_annot * EConstr.types) Tac2dyn.Val.tag

Sourceval val_free : Names.Id.Set.t Tac2dyn.Val.tag

Sourceval val_uint63 : Uint63.t Tac2dyn.Val.tag

Sourceval val_float : Float64.t Tac2dyn.Val.tag

Sourceval val_ltac1 : Geninterp.Val.t Tac2dyn.Val.tag

Sourceval val_pretype_flags : Pretyping.inference_flags Tac2dyn.Val.tag

Sourceval val_expected_type : Pretyping.typing_constraint Tac2dyn.Val.tag

Source

val val_ind_data : 
  (Names.Ind.t * Declarations.mutual_inductive_body) Tac2dyn.Val.tag

Sourceval val_transparent_state : TransparentState.t Tac2dyn.Val.tag

Sourceval val_exninfo : Exninfo.info Tac2dyn.Val.tag

Sourceval val_exn : Exninfo.iexn 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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac2_plugin/Ltac2_plugin/Tac2ffi/index.html

Module `Ltac2_plugin.Tac2ffi`Source

Ltac2 FFI

Dynamic tags

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac2_plugin/Ltac2_plugin/Tac2ffi/index.html

Module Ltac2_plugin.Tac2ffiSource

Ltac2 FFI

Dynamic tags

Module `Ltac2_plugin.Tac2ffi`Source