package coq-serapi

You can search for identifiers within the package.

in-package search v0.2.0

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

Module Serlib_funind.Ser_g_indfunSource

Module `Serlib_funind.Ser_g_indfun`Source