package coq-serapi
Serialization library and protocol for machine interaction with the Coq proof assistant
Install
Dune Dependency
Authors
Maintainers
Sources
coq-serapi-8.10.0.0.7.2.tbz
sha256=39018932b0520cc042246a3f9e03f3788d1aaff65568b480d8681cba235032e9
sha512=62a3bb3950e5f9d9cfa5fca85a1108a04fd8c1833cba560ff9d52246ef96d3d61a4743e6dc6d52f53c6a495040fad53f1d9aae383609227a6eb84568ad2a1a6c
doc/serlib_setoid_ring/Ser_g_newring/index.html
Module Ser_g_newring
module CAst = Serlib.Ser_cAstmodule Libnames = Serlib.Ser_libnamesmodule Constrexpr = Serlib.Ser_constrexprmodule Tactypes = Serlib.Ser_tactypesmodule Genintern = Serlib.Ser_geninternmodule EConstr = Serlib.Ser_eConstrmodule Tacexpr = Ser_tacexprmodule Ltac_plugin : sig ... endval coeff_spec_of_sexp :
'constr. (Ppx_sexp_conv_lib.Sexp.t -> 'constr) ->
Ppx_sexp_conv_lib.Sexp.t ->
'constr coeff_specval sexp_of_coeff_spec :
'constr. ('constr -> Ppx_sexp_conv_lib.Sexp.t) ->
'constr coeff_spec ->
Ppx_sexp_conv_lib.Sexp.ttype cst_tac_spec = Newring_plugin.Newring_ast.cst_tac_spec = | CstTac of Ltac_plugin.Tacexpr.raw_tactic_expr| Closed of Libnames.qualid list
val cst_tac_spec_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> cst_tac_specval sexp_of_cst_tac_spec : cst_tac_spec -> Ppx_sexp_conv_lib.Sexp.ttype 'constr ring_mod = 'constr Newring_plugin.Newring_ast.ring_mod = | Ring_kind of 'constr coeff_spec| Const_tac of cst_tac_spec| Pre_tac of Ltac_plugin.Tacexpr.raw_tactic_expr| Post_tac of Ltac_plugin.Tacexpr.raw_tactic_expr| Setoid of Constrexpr.constr_expr * Constrexpr.constr_expr| Pow_spec of cst_tac_spec * Constrexpr.constr_expr| Sign_spec of Constrexpr.constr_expr| Div_spec of Constrexpr.constr_expr
val ring_mod_of_sexp :
'constr. (Ppx_sexp_conv_lib.Sexp.t -> 'constr) ->
Ppx_sexp_conv_lib.Sexp.t ->
'constr ring_modval sexp_of_ring_mod :
'constr. ('constr -> Ppx_sexp_conv_lib.Sexp.t) ->
'constr ring_mod ->
Ppx_sexp_conv_lib.Sexp.ttype 'a field_mod = 'a Newring_plugin.Newring_ast.field_mod = | Ring_mod of 'a ring_mod| Inject of Constrexpr.constr_expr
val field_mod_of_sexp :
'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
Ppx_sexp_conv_lib.Sexp.t ->
'a field_modval sexp_of_field_mod :
'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
'a field_mod ->
Ppx_sexp_conv_lib.Sexp.tval ser_wit_field_mod :
(Constrexpr.constr_expr field_mod, unit, unit) Serlib.Ser_genarg.gen_serval ser_wit_field_mods :
(Constrexpr.constr_expr field_mod list, unit, unit) Serlib.Ser_genarg.gen_serval ser_wit_ring_mod :
(Constrexpr.constr_expr ring_mod, unit, unit) Serlib.Ser_genarg.gen_serval ser_wit_ring_mods :
(Constrexpr.constr_expr ring_mod list, unit, unit) Serlib.Ser_genarg.gen_ser