Module `Serlib_ssr.Ser_ssrparser`Source

Sourcemodule Ssrmatching = Serlib_ssrmatching.Ser_ssrmatching

Sourcemodule Ltac_plugin : sig ... end

Sourcemodule Ssrast = Ser_ssrast

Sourcemodule Ssreflect_plugin : sig ... end

Sourcetype t_movearg = Ssrmatching.cpattern Ssrast.ssragens Ssrast.ssrmovearg

Sourceval t_movearg_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> t_movearg

Sourceval sexp_of_t_movearg : t_movearg -> Ppx_sexp_conv_lib.Sexp.t

val ser_wit_ssrmovearg : 
  (t_movearg, t_movearg, t_movearg) Serlib.Ser_genarg.gen_ser

Source

val ser_wit_ssrapplyarg : 
  (Ssrast.ssrapplyarg, Ssrast.ssrapplyarg, Ssrast.ssrapplyarg)
    Serlib.Ser_genarg.gen_ser

Source

val ser_wit_clauses : 
  (Ssrast.clauses, Ssrast.clauses, Ssrast.clauses) Serlib.Ser_genarg.gen_ser

Sourcetype t_rwarg = Ssreflect_plugin.Ssrequality.ssrrwarg list

Sourceval t_rwarg_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> t_rwarg

Sourceval sexp_of_t_rwarg : t_rwarg -> Ppx_sexp_conv_lib.Sexp.t

Sourceval ser_wit_ssrrwargs : (t_rwarg, t_rwarg, t_rwarg) Serlib.Ser_genarg.gen_ser

Sourcetype t_h1 = Ssrast.Ltac_plugin.Tacexpr.raw_tactic_expr Ssrast.fwdbinders

Sourceval t_h1_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> t_h1

Sourceval sexp_of_t_h1 : t_h1 -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype t_h2 = Ssrast.Ltac_plugin.Tacexpr.glob_tactic_expr Ssrast.fwdbinders

Sourceval t_h2_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> t_h2

Sourceval sexp_of_t_h2 : t_h2 -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype t_h3 = Ssrast.Geninterp.Val.t Ssrast.fwdbinders

Sourceval t_h3_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> t_h3

Sourceval sexp_of_t_h3 : t_h3 -> Ppx_sexp_conv_lib.Sexp.t

Sourceval ser_wit_ssrhavefwdwbinders : (t_h1, t_h2, t_h3) Serlib.Ser_genarg.gen_ser

Sourcetype ssrfwdview = Ssreflect_plugin.Ssrast.ast_closure_term list

Sourceval ssrfwdview_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrfwdview

Sourceval sexp_of_ssrfwdview : ssrfwdview -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype ssreqid = Ssreflect_plugin.Ssrast.ssripat option

Sourceval ssreqid_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssreqid

Sourceval sexp_of_ssreqid : ssreqid -> Ppx_sexp_conv_lib.Sexp.t

Source

type ssrarg =
  ssrfwdview
  * (ssreqid
     * (Ssrast.Ssrmatching_plugin.Ssrmatching.cpattern
          Ssreflect_plugin.Ssrast.ssragens
        * Ssreflect_plugin.Ssrast.ssripats))

Sourceval ssrarg_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrarg

Sourceval sexp_of_ssrarg : ssrarg -> Ppx_sexp_conv_lib.Sexp.t

Sourceval ser_wit_ssrarg : (ssrarg, ssrarg, ssrarg) Serlib.Ser_genarg.gen_ser

Sourcetype h_h1 = Ssrast.Ltac_plugin.Tacexpr.raw_tactic_expr Ssrast.ssrhint

Sourceval h_h1_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> h_h1

Sourceval sexp_of_h_h1 : h_h1 -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype h_h2 = Ssrast.Ltac_plugin.Tacexpr.glob_tactic_expr Ssrast.ssrhint

Sourceval h_h2_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> h_h2

Sourceval sexp_of_h_h2 : h_h2 -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype h_h3 = Ssrast.Geninterp.Val.t Ssrast.ssrhint

Sourceval h_h3_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> h_h3

Sourceval sexp_of_h_h3 : h_h3 -> Ppx_sexp_conv_lib.Sexp.t

Sourceval ser_wit_ssrhintarg : (h_h1, h_h2, h_h3) Serlib.Ser_genarg.gen_ser

Sourcemodule A1 : sig ... end

Sourceval ser_wit_ssrseqarg : (A1.h1, A1.h2, A1.h3) Serlib.Ser_genarg.gen_ser

Sourcemodule A2 : sig ... end

Sourceval ser_wit_ssrintrosarg : (A2.h1, A2.h2, A2.h3) Serlib.Ser_genarg.gen_ser

Sourcemodule A3 : sig ... end

Sourceval ser_wit_ssrsufffwd : (A3.h1, A3.h2, A3.h3) Serlib.Ser_genarg.gen_ser

Sourcemodule A4 : sig ... end

Sourceval ser_wit_ssrcongrarg : (A4.h1, A4.h1, A4.h1) Serlib.Ser_genarg.gen_ser

Sourcemodule A5 : sig ... end

Sourceval ser_wit_ssrdoarg : (A5.h1, A5.h2, A5.h3) Serlib.Ser_genarg.gen_ser

Sourcemodule A6 : sig ... end

Sourceval ser_wit_ssrsetfwd : (A6.h1, A6.h1, A6.h1) Serlib.Ser_genarg.gen_ser

Sourcemodule A7 : sig ... end

Sourceval ser_wit_ssrhint : (A7.h1, A7.h2, A7.h3) Serlib.Ser_genarg.gen_ser

Sourcemodule A8 : sig ... end

Sourceval ser_wit_ssrposefwd : (A8.h1, A8.h1, A8.h1) Serlib.Ser_genarg.gen_ser

Sourcemodule A9 : sig ... end

Sourceval ser_wit_ssrunlockarg : (A9.h1, A9.h1, A9.h1) Serlib.Ser_genarg.gen_ser

Sourcemodule A10 : sig ... end

Sourceval ser_wit_ssrwlogfwd : (A10.h1, A10.h1, A10.h1) Serlib.Ser_genarg.gen_ser

Sourcemodule A11 : sig ... end

Sourceval ser_wit_ssrfixfwd : (A11.h1, A11.h1, A11.h1) Serlib.Ser_genarg.gen_ser

Sourcemodule A12 : sig ... end

Sourceval ser_wit_ssrfwd : (A12.h1, A12.h1, A12.h1) Serlib.Ser_genarg.gen_ser

Sourceval register : unit -> unit

Install

Dune Dependency

Authors

Maintainers

Sources

doc/serlib_ssr/Serlib_ssr/Ser_ssrparser/index.html

Module `Serlib_ssr.Ser_ssrparser`Source

package coq-serapi

Install

Dune Dependency

Authors

Maintainers

Sources

doc/serlib_ssr/Serlib_ssr/Ser_ssrparser/index.html

Module Serlib_ssr.Ser_ssrparserSource

Module `Serlib_ssr.Ser_ssrparser`Source