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

sha256=530991b3e029102367184b96d8bd8a347c7172265a5815176a533b1061f8c6cf

sha512=c6cc5afcad3546c3fbcd8512f20a5ebd748f17529805c1d296959092fde8f31b77f7c7a06254f68c30eb6c6ad520bfbf03388505186a600e75d65ae3acd02c77

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