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.0.tbz
sha256=4448c2b45a6975d7a90d3e07ce75386103d3e17c8ad96c566da854ac1e56802c
sha512=19027ca59703c8b74abd372e14403d22d07e9e8c248a50ae8f880647c10ee1f22cee93587583374c96971a667e10546b4997ff7b6a91aea51b51bbacb3052ee4
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