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

sha256=e252d05b41e920c1df4343c437be4018804971ecfd00291ddb4d31ce72281853

sha512=1f936181265346d0cd17ec292b98f201382ea84440b415b77664430044ba599072e653366f080d8b63ee5f8fe5bfc0d2cd2a38cc759532500d8c60a483fe36b7

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 : 
  Sexplib0.Sexp.t ->
  function_fix_definition_loc_argtype

Source

val sexp_of_function_fix_definition_loc_argtype : 
  function_fix_definition_loc_argtype ->
  Sexplib0.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