package coq-serapi
Serialization library and protocol for machine interaction with the Coq proof assistant
Install
dune-project
Dependency
Authors
Maintainers
Sources
coq-serapi-8.11.0+0.11.1.tbz
sha256=f06bb0ab1041ac6f8d73faddda404827ce94b6b3310483e93d7fd18bd018e1ed
sha512=ecbed7b5b8451f65d40bf50fd1471b5038029c6f1ae8912c8cb51e61699cc4c158bc4f3533ec5f0898d1fc3d91683c0ff815fa44be7fdaedea59b71ca1d1b7d3
doc/serlib_ssr/Serlib_ssr/Ser_ssrparser/index.html
Module Serlib_ssr.Ser_ssrparser
module Ssrmatching = Serlib_ssrmatching.Ser_ssrmatchingmodule Ltac_plugin : sig ... endmodule Ssrast = Ser_ssrastmodule Ssreflect_plugin : sig ... endtype t_movearg = Ssrmatching.cpattern Ssrast.ssragens Ssrast.ssrmoveargval t_movearg_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> t_moveargval sexp_of_t_movearg : t_movearg -> Ppx_sexp_conv_lib.Sexp.tval ser_wit_ssrmovearg :
(t_movearg, t_movearg, t_movearg) Serlib.Ser_genarg.gen_serval ser_wit_ssrapplyarg :
(Ssrast.ssrapplyarg, Ssrast.ssrapplyarg, Ssrast.ssrapplyarg)
Serlib.Ser_genarg.gen_serval ser_wit_clauses :
(Ssrast.clauses, Ssrast.clauses, Ssrast.clauses) Serlib.Ser_genarg.gen_sertype t_rwarg = Ssreflect_plugin.Ssrequality.ssrrwarg listval t_rwarg_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> t_rwargval sexp_of_t_rwarg : t_rwarg -> Ppx_sexp_conv_lib.Sexp.tval ser_wit_ssrrwargs : (t_rwarg, t_rwarg, t_rwarg) Serlib.Ser_genarg.gen_serval t_h1_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> t_h1val sexp_of_t_h1 : t_h1 -> Ppx_sexp_conv_lib.Sexp.tval t_h2_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> t_h2val sexp_of_t_h2 : t_h2 -> Ppx_sexp_conv_lib.Sexp.ttype t_h3 = Ssrast.Geninterp.Val.t Ssrast.fwdbindersval t_h3_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> t_h3val sexp_of_t_h3 : t_h3 -> Ppx_sexp_conv_lib.Sexp.tval ser_wit_ssrhavefwdwbinders : (t_h1, t_h2, t_h3) Serlib.Ser_genarg.gen_sertype ssrfwdview = Ssrast.ast_closure_term listval ssrfwdview_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrfwdviewval sexp_of_ssrfwdview : ssrfwdview -> Ppx_sexp_conv_lib.Sexp.ttype ssreqid = Ssrast.ssripat optionval ssreqid_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssreqidval sexp_of_ssreqid : ssreqid -> Ppx_sexp_conv_lib.Sexp.ttype ssrarg =
ssrfwdview
* (ssreqid
* (Ssrast.Ssrmatching_plugin.Ssrmatching.cpattern Ssrast.ssragens
* Ssrast.ssripats))val ssrarg_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrargval sexp_of_ssrarg : ssrarg -> Ppx_sexp_conv_lib.Sexp.tval ser_wit_ssrarg : (ssrarg, ssrarg, ssrarg) Serlib.Ser_genarg.gen_serval h_h1_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> h_h1val sexp_of_h_h1 : h_h1 -> Ppx_sexp_conv_lib.Sexp.tval h_h2_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> h_h2val sexp_of_h_h2 : h_h2 -> Ppx_sexp_conv_lib.Sexp.ttype h_h3 = Ssrast.Geninterp.Val.t Ssrast.ssrhintval h_h3_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> h_h3val sexp_of_h_h3 : h_h3 -> Ppx_sexp_conv_lib.Sexp.tval ser_wit_ssrhintarg : (h_h1, h_h2, h_h3) Serlib.Ser_genarg.gen_sermodule A1 : sig ... endval ser_wit_ssrseqarg : (A1.h1, A1.h2, A1.h3) Serlib.Ser_genarg.gen_sermodule A2 : sig ... endval ser_wit_ssrintrosarg : (A2.h1, A2.h2, A2.h3) Serlib.Ser_genarg.gen_sermodule A3 : sig ... endval ser_wit_ssrsufffwd : (A3.h1, A3.h2, A3.h3) Serlib.Ser_genarg.gen_sermodule A4 : sig ... endval ser_wit_ssrcongrarg : (A4.h1, A4.h1, A4.h1) Serlib.Ser_genarg.gen_sermodule A5 : sig ... endval ser_wit_ssrdoarg : (A5.h1, A5.h2, A5.h3) Serlib.Ser_genarg.gen_sermodule A6 : sig ... endval ser_wit_ssrsetfwd : (A6.h1, A6.h1, A6.h1) Serlib.Ser_genarg.gen_sermodule A7 : sig ... endval ser_wit_ssrhint : (A7.h1, A7.h2, A7.h3) Serlib.Ser_genarg.gen_sermodule A8 : sig ... endval ser_wit_ssrposefwd : (A8.h1, A8.h1, A8.h1) Serlib.Ser_genarg.gen_sermodule A9 : sig ... endval ser_wit_ssrunlockarg : (A9.h1, A9.h1, A9.h1) Serlib.Ser_genarg.gen_sermodule A10 : sig ... endval ser_wit_ssrwlogfwd : (A10.h1, A10.h1, A10.h1) Serlib.Ser_genarg.gen_sermodule A11 : sig ... endval ser_wit_ssrfixfwd : (A11.h1, A11.h1, A11.h1) Serlib.Ser_genarg.gen_sermodule A12 : sig ... endval ser_wit_ssrfwd : (A12.h1, A12.h1, A12.h1) Serlib.Ser_genarg.gen_ser