To focus the search input from anywhere on the page, press the 'S' key.
in-package search v0.1.0
package coq-serapi
-
coq-serapi.serapi_v8_14
-
coq-serapi.serlib
-
-
coq-serapi.serlib.extraction_plugin
-
coq-serapi.serlib.firstorder_plugin
-
coq-serapi.serlib.funind_plugin
-
coq-serapi.serlib.ltac
-
coq-serapi.serlib.ring_plugin
-
coq-serapi.serlib.ssreflect_plugin
-
coq-serapi.serlib.ssrmatching_plugin
-
coq-serapi.sertop_v8_12
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
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 = Serlib_ltac.Ser_tacexprmodule Ltac_plugin : sig ... endtype 'constr coeff_spec = 'constr Ring_plugin.Ring_ast.coeff_spec = val 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 = Ring_plugin.Ring_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 Ring_plugin.Ring_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 Ring_plugin.Ring_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