package coq-serapi

You can search for identifiers within the package.

in-package search v0.2.0

package coq-serapi

coq-serapi.serlib
- SerType
  - S
  - S1
- Ser_bigint
- Ser_cAst
- Ser_cEphemeron
- Ser_cMap
  - ExtS
  - Make
    
    M
    
    S
- Ser_cSet
  - ExtS
  - Make
    
    M
    
    S
- Ser_cemitcodes
- Ser_class_tactics
- Ser_constr
- Ser_constr_matching
- Ser_constrexpr
- Ser_context
  - Compacted
    
    Declaration
  - Named
    
    Declaration
  - Rel
    
    Declaration
- Ser_conv_oracle
- Ser_cooking
- Ser_dAst
- Ser_decl_kinds
- Ser_declarations
- Ser_declaremods
- Ser_eConstr
- Ser_entries
- Ser_environ
- Ser_equality
- Ser_evar
  - Self
  - Set
- Ser_evar_kinds
- Ser_evd
- Ser_extend
- Ser_feedback
- Ser_flags
- Ser_future
- Ser_genarg
- Ser_genintern
- Ser_geninterp
  - Val
- Ser_genredexpr
- Ser_glob_term
- Ser_goal
- Ser_goal_select
- Ser_goptions
- Ser_hints
- Ser_impargs
- Ser_int
- Ser_inv
- Ser_libnames
- Ser_library
- Ser_loc
- Ser_locus
- Ser_ltac_pretype
- Ser_mltop
- Ser_mod_subst
- Ser_namegen
- Ser_names
  - Cmap
  - Cmap_env
  - Constant
  - DirPath
  - GlobRef
  - Id
    
    Map
    
    Set
  - KerName
  - Label
  - MBId
  - MPmap
  - Mindmap
  - Mindmap_env
  - ModPath
  - MutInd
  - Name
  - Projection
    
    Repr
- Ser_nametab
- Ser_notation
- Ser_notation_gram
- Ser_notation_term
- Ser_opaqueproof
- Ser_pattern
- Ser_pp
- Ser_ppextend
- Ser_pretype_errors
- Ser_printer
- Ser_proof
- Ser_proof_bullet
- Ser_proof_global
- Ser_range
- Ser_reduction
- Ser_retroknowledge
- Ser_rtree
- Ser_safe_typing
- Ser_sorts
- Ser_stateid
- Ser_stdarg
- Ser_stm
- Ser_tactics
- Ser_tactypes
- Ser_tok
- Ser_type_errors
- Ser_typeclasses
- Ser_uGraph
- Ser_uState
- Ser_univ
- Ser_univNames
- Ser_universes
- Ser_util
- Ser_vernacexpr
- Ser_vernacinterp
- Ser_vmvalues
- Ser_xml_datatype
- Serlib_base
- Serlib_init
coq-serapi.serlib.ground_plugin
- Ser_g_ground
coq-serapi.serlib.ltac
coq-serapi.serlib.newring_plugin
- Ser_g_newring
  - Ltac_plugin
coq-serapi.serlib.recdef_plugin
- Ser_g_indfun
  - A1
  - A2

Legend:
Library
Module
Module type
Parameter
Class
Class type

type rlevel = Genarg.rlevel

type glevel = Genarg.glevel

type tlevel = Genarg.tlevel

val rlevel_of_sexp : Sexplib.Sexp.t -> rlevel

val sexp_of_rlevel : rlevel -> Sexplib.Sexp.t

val glevel_of_sexp : Sexplib.Sexp.t -> glevel

val sexp_of_glevel : glevel -> Sexplib.Sexp.t

val tlevel_of_sexp : Sexplib.Sexp.t -> tlevel

val sexp_of_tlevel : tlevel -> Sexplib.Sexp.t

type 'a generic_argument = 'a Genarg.generic_argument

val generic_argument_of_sexp : 
  (Sexplib.Sexp.t -> 'a) ->
  Sexplib.Sexp.t ->
  'a Genarg.generic_argument

val sexp_of_generic_argument : 
  ('a -> Sexplib.Sexp.t) ->
  'a Genarg.generic_argument ->
  Sexplib.Sexp.t

type glob_generic_argument = Genarg.glob_generic_argument

val glob_generic_argument_of_sexp : 
  Sexplib.Sexp.t ->
  Genarg.glob_generic_argument

val sexp_of_glob_generic_argument : 
  Genarg.glob_generic_argument ->
  Sexplib.Sexp.t

type raw_generic_argument = Genarg.raw_generic_argument

val raw_generic_argument_of_sexp : 
  Sexplib.Sexp.t ->
  Genarg.raw_generic_argument

val sexp_of_raw_generic_argument : 
  Genarg.raw_generic_argument ->
  Sexplib.Sexp.t

type typed_generic_argument = Genarg.typed_generic_argument

val typed_generic_argument_of_sexp : 
  Sexplib.Sexp.t ->
  Genarg.typed_generic_argument

val sexp_of_typed_generic_argument : 
  Genarg.typed_generic_argument ->
  Sexplib.Sexp.t

type ('raw, 'glb, 'top) gen_ser = {

raw_ser : 'raw -> Sexplib.Sexp.t;
raw_des : Sexplib.Sexp.t -> 'raw;
glb_ser : 'glb -> Sexplib.Sexp.t;
glb_des : Sexplib.Sexp.t -> 'glb;
top_ser : 'top -> Sexplib.Sexp.t;
top_des : Sexplib.Sexp.t -> 'top;

}

val register_genser : 
  ('raw, 'glb, 'top) Genarg.genarg_type ->
  ('raw, 'glb, 'top) gen_ser ->
  unit

val mk_uniform : 
  ('t -> Sexplib.Sexp.t) ->
  (Sexplib.Sexp.t -> 't) ->
  ('t, 't, 't) gen_ser