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.1.tbz
sha256=207b091d8d9d9e1a649759f0acfd15cbfda54a2627a01fc74aa74ec0ffaa3400
sha512=af85d00c5896e78a6edea7794070795ca14c8e47a0e9a28f2ac003364b0f99eb72f19f57e755a3967d255b1aaf62cae0d09bbab02d2d35ef6ee02b84823a0929
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