Ltac2_plugin.Tac2ffival repr_of : 'a repr -> 'a -> Tac2val.valexprval repr_to : 'a repr -> Tac2val.valexpr -> 'aval make_repr : ('a -> Tac2val.valexpr) -> (Tac2val.valexpr -> 'a) -> 'a reprThese 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.valexprval to_unit : Tac2val.valexpr -> unitval unit : unit reprval of_int : int -> Tac2val.valexprval to_int : Tac2val.valexpr -> intval int : int reprval of_bool : bool -> Tac2val.valexprval to_bool : Tac2val.valexpr -> boolval bool : bool reprval of_char : char -> Tac2val.valexprval to_char : Tac2val.valexpr -> charval char : char reprval of_bytes : Stdlib.Bytes.t -> Tac2val.valexprval to_bytes : Tac2val.valexpr -> Stdlib.Bytes.tval bytes : Stdlib.Bytes.t reprval of_string : string -> Tac2val.valexprWARNING these functions copy
val to_string : Tac2val.valexpr -> stringval string : string reprval of_list : ('a -> Tac2val.valexpr) -> 'a list -> Tac2val.valexprval to_list : (Tac2val.valexpr -> 'a) -> Tac2val.valexpr -> 'a listval of_constr : EConstr.t -> Tac2val.valexprval to_constr : Tac2val.valexpr -> EConstr.tval of_matching_context : Constr_matching.context -> Tac2val.valexprval to_matching_context : Tac2val.valexpr -> Constr_matching.contextval matching_context : Constr_matching.context reprval of_preterm : Ltac_pretype.closed_glob_constr -> Tac2val.valexprval to_preterm : Tac2val.valexpr -> Ltac_pretype.closed_glob_constrval preterm : Ltac_pretype.closed_glob_constr reprval of_cast : Constr.cast_kind -> Tac2val.valexprval to_cast : Tac2val.valexpr -> Constr.cast_kindval cast : Constr.cast_kind reprval of_err : Exninfo.iexn -> Tac2val.valexprToplevel representation of OCaml exceptions. Invariant: no LtacError should be used with err.
val to_err : Tac2val.valexpr -> Exninfo.iexnval err : Exninfo.iexn reprval of_exn : Exninfo.iexn -> Tac2val.valexprval to_exn : Tac2val.valexpr -> Exninfo.iexnval exn : Exninfo.iexn reprval of_exninfo : Exninfo.info -> Tac2val.valexprval to_exninfo : Tac2val.valexpr -> Exninfo.infoval exninfo : Exninfo.info reprval of_result : ('a -> Tac2val.valexpr) -> ('a, Exninfo.iexn) Stdlib.result -> Tac2val.valexprval to_result : (Tac2val.valexpr -> 'a) -> Tac2val.valexpr -> ('a, Exninfo.iexn) Stdlib.resultval result : 'a repr -> ('a, Exninfo.iexn) Stdlib.result reprval of_ident : Names.Id.t -> Tac2val.valexprval to_ident : Tac2val.valexpr -> Names.Id.tval ident : Names.Id.t reprval of_closure : Tac2val.closure -> Tac2val.valexprval to_closure : Tac2val.valexpr -> Tac2val.closureval closure : Tac2val.closure reprtype ('a, 'b) fun1 = 'a -> 'b Proofview.tacticval of_fun1 : (Tac2val.valexpr -> 'a) -> ('b -> Tac2val.valexpr) -> ('a, 'b) fun1 -> Tac2val.valexprval to_fun1 : ('a -> Tac2val.valexpr) -> (Tac2val.valexpr -> 'b) -> Tac2val.valexpr -> ('a, 'b) fun1type ('a, 'b, 'c) fun2 = 'a -> 'b -> 'c Proofview.tacticval of_fun2 : (Tac2val.valexpr -> 'a) -> (Tac2val.valexpr -> 'b) -> ('c -> Tac2val.valexpr) -> ('a, 'b, 'c) fun2 -> Tac2val.valexprval to_fun2 : ('a -> Tac2val.valexpr) -> ('b -> Tac2val.valexpr) -> (Tac2val.valexpr -> 'c) -> Tac2val.valexpr -> ('a, 'b, 'c) fun2val of_block : (int * Tac2val.valexpr array) -> Tac2val.valexprval to_block : Tac2val.valexpr -> int * Tac2val.valexpr arrayval block : (int * Tac2val.valexpr array) reprval of_array : ('a -> Tac2val.valexpr) -> 'a array -> Tac2val.valexprval to_array : (Tac2val.valexpr -> 'a) -> Tac2val.valexpr -> 'a arrayval of_tuple : Tac2val.valexpr array -> Tac2val.valexprval to_tuple : Tac2val.valexpr -> Tac2val.valexpr arrayval of_pair : ('a -> Tac2val.valexpr) -> ('b -> Tac2val.valexpr) -> ('a * 'b) -> Tac2val.valexprval to_pair : (Tac2val.valexpr -> 'a) -> (Tac2val.valexpr -> 'b) -> Tac2val.valexpr -> 'a * 'bval of_triple : ('a -> Tac2val.valexpr) -> ('b -> Tac2val.valexpr) -> ('c -> Tac2val.valexpr) -> ('a * 'b * 'c) -> Tac2val.valexprval to_triple : (Tac2val.valexpr -> 'a) -> (Tac2val.valexpr -> 'b) -> (Tac2val.valexpr -> 'c) -> Tac2val.valexpr -> 'a * 'b * 'cval of_option : ('a -> Tac2val.valexpr) -> 'a option -> Tac2val.valexprval to_option : (Tac2val.valexpr -> 'a) -> Tac2val.valexpr -> 'a optionval of_pattern : Pattern.constr_pattern -> Tac2val.valexprval to_pattern : Tac2val.valexpr -> Pattern.constr_patternval pattern : Pattern.constr_pattern reprval of_evar : Evar.t -> Tac2val.valexprval to_evar : Tac2val.valexpr -> Evar.tval of_sort : EConstr.ESorts.t -> Tac2val.valexprval to_sort : Tac2val.valexpr -> EConstr.ESorts.tval sort : EConstr.ESorts.t reprval of_reduction : Redexpr.red_expr -> Tac2val.valexprval to_reduction : Tac2val.valexpr -> Redexpr.red_exprval reduction : Redexpr.red_expr reprval of_rewstrategy : Rewrite.strategy -> Tac2val.valexprval to_rewstrategy : Tac2val.valexpr -> Rewrite.strategyval rewstrategy : Rewrite.strategy reprval of_pp : Pp.t -> Tac2val.valexprval to_pp : Tac2val.valexpr -> Pp.tval of_transparent_state : TransparentState.t -> Tac2val.valexprval to_transparent_state : Tac2val.valexpr -> TransparentState.tval transparent_state : TransparentState.t reprval of_pretype_flags : Pretyping.inference_flags -> Tac2val.valexprval to_pretype_flags : Tac2val.valexpr -> Pretyping.inference_flagsval pretype_flags : Pretyping.inference_flags reprval of_expected_type : Pretyping.typing_constraint -> Tac2val.valexprval to_expected_type : Tac2val.valexpr -> Pretyping.typing_constraintval expected_type : Pretyping.typing_constraint reprtype ind_data = Names.Ind.t * Declarations.mutual_inductive_bodyval of_ind_data : ind_data -> Tac2val.valexprval to_ind_data : Tac2val.valexpr -> ind_dataval of_inductive : Names.inductive -> Tac2val.valexprval to_inductive : Tac2val.valexpr -> Names.inductiveval inductive : Names.inductive reprval of_constant : Names.Constant.t -> Tac2val.valexprval to_constant : Tac2val.valexpr -> Names.Constant.tval constant : Names.Constant.t reprval of_constructor : Names.constructor -> Tac2val.valexprval to_constructor : Tac2val.valexpr -> Names.constructorval constructor : Names.constructor reprval of_projection : Names.Projection.t -> Tac2val.valexprval to_projection : Tac2val.valexpr -> Names.Projection.tval projection : Names.Projection.t reprval of_qvar : Sorts.QVar.t -> Tac2val.valexprval to_qvar : Tac2val.valexpr -> Sorts.QVar.tval qvar : Sorts.QVar.t reprval of_case : Constr.case_info -> Tac2val.valexprval to_case : Tac2val.valexpr -> Constr.case_infoval case : Constr.case_info reprtype binder = Names.Name.t EConstr.binder_annot * EConstr.typesval of_binder : binder -> Tac2val.valexprval to_binder : Tac2val.valexpr -> binderval of_instance : EConstr.EInstance.t -> Tac2val.valexprval to_instance : Tac2val.valexpr -> EConstr.EInstance.tval instance : EConstr.EInstance.t reprval of_reference : Names.GlobRef.t -> Tac2val.valexprval to_reference : Tac2val.valexpr -> Names.GlobRef.tval reference : Names.GlobRef.t reprval of_ext : 'a Tac2dyn.Val.tag -> 'a -> Tac2val.valexprval to_ext : 'a Tac2dyn.Val.tag -> Tac2val.valexpr -> 'aval repr_ext : 'a Tac2dyn.Val.tag -> 'a reprval of_open : (Names.KerName.t * Tac2val.valexpr array) -> Tac2val.valexprval to_open : Tac2val.valexpr -> Names.KerName.t * Tac2val.valexpr arrayval open_ : (Names.KerName.t * Tac2val.valexpr array) reprval of_free : Nameops.Fresh.t -> Tac2val.valexprval to_free : Tac2val.valexpr -> Nameops.Fresh.tval free : Nameops.Fresh.t reprval of_uint63 : Uint63.t -> Tac2val.valexprval to_uint63 : Tac2val.valexpr -> Uint63.tval of_float : Float64.t -> Tac2val.valexprval to_float : Tac2val.valexpr -> Float64.tval of_pstring : Pstring.t -> Tac2val.valexprval to_pstring : Tac2val.valexpr -> Pstring.tval valexpr : Tac2val.valexpr reprException
exception LtacError of Names.KerName.t * Tac2val.valexpr arrayLtac2-defined exceptions seen from OCaml side
Standard exceptions