package coq-serapi

You can search for identifiers within the package.

in-package search v0.2.0

Serialization library and protocol for machine interaction with the Coq proof assistant

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (38)

Authors

Maintainers

E

e@x80.org

Sources

coq-serapi-8.13.0.0.13.0.tbz

sha256=ddef1d7278021ce391f62e8e222e10962c7a308d6a2dfd8320382b4cf9a8cd75

sha512=8ee9cc09e5b8708b6cd7b0af8fccaa900413aa106cb47d99ca1fdd5b39c52676fa906204766f8f9e0964cc7e3ef987009de79f26b534b2021cf66f20c3d62bfe

doc/serlib_funind/Serlib_funind/Ser_g_indfun/index.html

Module `Serlib_funind.Ser_g_indfun`Source

Sourcemodule CAst = Serlib.Ser_cAst

Sourcemodule Constrexpr = Serlib.Ser_constrexpr

Sourcemodule Tactypes = Serlib.Ser_tactypes

Sourcemodule Genintern = Serlib.Ser_genintern

Sourcemodule EConstr = Serlib.Ser_eConstr

Sourcemodule Tacexpr = Serlib_ltac.Ser_tacexpr

Sourcemodule A1 : sig ... end

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

Sourcemodule A2 : sig ... end

Source

val ser_wit_fun_ind_using : 
  (Constrexpr.constr_expr Tactypes.with_bindings option,
    Genintern.glob_constr_and_expr Tactypes.with_bindings option,
    EConstr.t Tactypes.with_bindings Tactypes.delayed_open option)
    Serlib.Ser_genarg.gen_ser

Source

val ser_wit_fun_scheme_arg : 
  (Names.variable * Libnames.qualid * Sorts.family, unit, unit)
    Serlib.Ser_genarg.gen_ser

Sourcemodule Loc = Serlib.Ser_loc

Sourcemodule Vernacexpr = Serlib.Ser_vernacexpr

Sourcetype function_fix_definition_loc_argtype = Vernacexpr.fixpoint_expr Loc.located

Source

val function_fix_definition_loc_argtype_of_sexp : 
  Ppx_sexp_conv_lib.Sexp.t ->
  function_fix_definition_loc_argtype

Source

val sexp_of_function_fix_definition_loc_argtype : 
  function_fix_definition_loc_argtype ->
  Ppx_sexp_conv_lib.Sexp.t

Source

val ser_wit_function_fix_definition : 
  (function_fix_definition_loc_argtype,
    function_fix_definition_loc_argtype,
    function_fix_definition_loc_argtype)
    Serlib.Ser_genarg.gen_ser

Source

val ser_wit_auto_using' : 
  (Serlib.Ser_constrexpr.constr_expr list,
    Serlib.Ser_genintern.glob_constr_and_expr list,
    Serlib.Ser_eConstr.constr list)
    Serlib.Ser_genarg.gen_ser

Sourceval register : unit -> unit

package coq-serapi

Install

Dune Dependency

Authors

Maintainers

Sources

doc/serlib_funind/Serlib_funind/Ser_g_indfun/index.html

Module Serlib_funind.Ser_g_indfunSource

Module `Serlib_funind.Ser_g_indfun`Source