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.15.0.0.15.1.tbz

sha256=31d1e4661f5b1b917d7004c749cc05eb73546d3190ac632faddc37348531a0a5

sha512=a9816915f9dc4051e76c5b0e615b27c1bb0a6a5ffd445af94ad2ed1582a0e704a7f49f69b6764fa92dbfa092aa8e41ee3151a1330b394eb0338c796d6460fa20

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