package coq-serapi

You can search for identifiers within the package.

in-package search v0.2.0

coq-serapi.serapi_v8_13
- Serapi
coq-serapi.serlib
- Serlib
  - SerType
    
    S
    
    S1
    
    SJ
    
    SJ1
  - Ser_attributes
  - Ser_cAst
  - Ser_cEphemeron
  - Ser_cMap
    
    ExtS
    
    Make
    
    M
    
    S
  - Ser_cPrimitives
  - Ser_cSet
    
    ExtS
    
    ExtSJ
    
    Make
    
    M
    
    S
    
    MakeJ
    
    M
    
    S
  - Ser_cUnix
  - 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_declarations
  - Ser_declaremods
  - Ser_decls
  - Ser_deprecation
  - Ser_eConstr
  - Ser_entries
  - Ser_environ
  - Ser_equality
  - Ser_evar
    
    Self
    
    Set
  - Ser_evar_kinds
  - Ser_evd
  - Ser_extend
  - Ser_feedback
  - Ser_flags
  - Ser_float64
  - Ser_future
  - Ser_genarg
  - Ser_genintern
    
    Store
  - Ser_geninterp
    
    Val
  - Ser_genredexpr
  - Ser_glob_term
  - Ser_globnames
  - Ser_goal
  - Ser_goal_select
  - Ser_goptions
  - Ser_gramlib
    
    Gramext
  - Ser_hints
  - Ser_impargs
  - Ser_int
  - Ser_inv
  - Ser_libnames
  - Ser_loadpath
  - Ser_loc
  - Ser_locality
  - Ser_locus
  - Ser_ltac_pretype
  - Ser_mod_subst
  - Ser_namegen
  - Ser_names
    
    Cmap
    
    Cmap_env
    
    Constant
    
    DPmap
    
    DirPath
    
    GlobRef
    
    Id
    
    Map
    
    Set
    
    KerName
    
    Label
    
    MBId
    
    MPmap
    
    Mindmap
    
    Mindmap_env
    
    ModPath
    
    MutInd
    
    Name
    
    Projection
    
    Repr
  - Ser_nametab
  - Ser_nativevalues
  - Ser_notation
  - Ser_notation_gram
  - Ser_notation_term
  - Ser_numTok
    
    Signed
    
    Unsigned
  - Ser_opaqueproof
  - Ser_pattern
  - Ser_pp
  - Ser_ppextend
  - Ser_pretype_errors
  - Ser_printer
  - Ser_proof
  - Ser_proof_bullet
  - Ser_range
  - Ser_reduction
  - Ser_retroknowledge
  - Ser_rtree
  - Ser_safe_typing
  - Ser_sorts
  - Ser_stateid
    
    Self
  - Ser_stdarg
  - Ser_stdlib
    
    Lazy
  - Ser_stm
  - Ser_tactics
  - Ser_tactypes
  - Ser_tok
  - Ser_type_errors
  - Ser_typeclasses
  - Ser_uGraph
    
    Bound
  - Ser_uState
  - Ser_uint63
  - Ser_univ
    
    AUContext
    
    Constraint
    
    ContextSet
    
    Instance
    
    Level
    
    UContext
    
    Universe
    
    Variance
  - Ser_univNames
  - Ser_universes
  - Ser_util
  - Ser_vernacexpr
  - Ser_vernacextend
  - Ser_vmemitcodes
  - Ser_vmvalues
  - Ser_xml_datatype
  - Serlib_base
  - Serlib_init
coq-serapi.serlib.extraction_plugin
- Serlib_extraction
  - Ser_g_extraction
coq-serapi.serlib.ground_plugin
- Serlib_firstorder
  - Ser_g_ground
coq-serapi.serlib.ltac
- Serlib_ltac
coq-serapi.serlib.recdef_plugin
- Serlib_funind
  - Ser_g_indfun
    
    A1
    
    A2
coq-serapi.serlib.ring_plugin
- Serlib_ring
  - Ser_g_ring
    
    Ltac_plugin
coq-serapi.serlib.ssreflect_plugin
- Serlib_ssr
  - Ser_ssrast
    
    Ltac_plugin
    
    Proofview
    
    Ssrmatching_plugin
  - Ser_ssrequality
    
    Ssreflect_plugin
    
    Ssrmatching_plugin
  - Ser_ssrparser
    
    A1
    
    A10
    
    A11
    
    A12
    
    A2
    
    A3
    
    A4
    
    A5
    
    A6
    
    A7
    
    A8
    
    A9
    
    Ltac_plugin
    
    Ssreflect_plugin
  - Wrap_ssrast
    
    Ssreflect_plugin
    
    Wrap
coq-serapi.serlib.ssrmatching_plugin
- Serlib_ssrmatching
  - Ser_ssrmatching
coq-serapi.sertop_v8_12
- Sertop

Legend:
Library
Module
Module type
Parameter
Class
Class type

type binding_kind = Glob_term.binding_kind

val binding_kind_of_sexp : Sexplib.Sexp.t -> Glob_term.binding_kind

val sexp_of_binding_kind : Glob_term.binding_kind -> Sexplib.Sexp.t

val binding_kind_of_yojson : 
  Yojson.Safe.t ->
  (binding_kind, string) Stdlib.result

val binding_kind_to_yojson : Glob_term.binding_kind -> Yojson.Safe.t

type 'a glob_sort_gen = 'a Glob_term.glob_sort_gen

val glob_sort_gen_of_sexp : 
  (Sexplib.Sexp.t -> 'a) ->
  Sexplib.Sexp.t ->
  'a Glob_term.glob_sort_gen

val sexp_of_glob_sort_gen : 
  ('a -> Sexplib.Sexp.t) ->
  'a Glob_term.glob_sort_gen ->
  Sexplib.Sexp.t

val glob_sort_gen_of_yojson : 
  (Yojson.Safe.t -> ('a, string) Stdlib.result) ->
  Yojson.Safe.t ->
  ('a glob_sort_gen, string) Stdlib.result

val glob_sort_gen_to_yojson : 
  ('a -> Yojson.Safe.t) ->
  'a Glob_term.glob_sort_gen ->
  Yojson.Safe.t

type glob_level = Glob_term.glob_level

val glob_level_of_sexp : Sexplib.Sexp.t -> Glob_term.glob_level

val sexp_of_glob_level : Glob_term.glob_level -> Sexplib.Sexp.t

val glob_level_of_yojson : Yojson.Safe.t -> (glob_level, string) Stdlib.result

val glob_level_to_yojson : Glob_term.glob_level -> Yojson.Safe.t

type glob_sort = Glob_term.glob_sort

val glob_sort_of_sexp : Sexplib.Sexp.t -> Glob_term.glob_sort

val sexp_of_glob_sort : Glob_term.glob_sort -> Sexplib.Sexp.t

val glob_sort_of_yojson : Yojson.Safe.t -> (glob_sort, string) Result.result

val glob_sort_to_yojson : glob_sort -> Yojson.Safe.t

type 'a cast_type = 'a Glob_term.cast_type

val cast_type_of_sexp : 
  (Sexplib.Sexp.t -> 'a) ->
  Sexplib.Sexp.t ->
  'a Glob_term.cast_type

val sexp_of_cast_type : 
  ('a -> Sexplib.Sexp.t) ->
  'a Glob_term.cast_type ->
  Sexplib.Sexp.t

val cast_type_of_yojson : 
  (Yojson.Safe.t -> ('a, string) Stdlib.result) ->
  Yojson.Safe.t ->
  ('a cast_type, string) Result.result

val cast_type_to_yojson : 
  ('a -> Yojson.Safe.t) ->
  'a cast_type ->
  Yojson.Safe.t

type glob_constraint = Glob_term.glob_constraint

val glob_constraint_of_sexp : Sexplib.Sexp.t -> Glob_term.glob_constraint

val sexp_of_glob_constraint : Glob_term.glob_constraint -> Sexplib.Sexp.t

val glob_constraint_of_yojson : 
  Yojson.Safe.t ->
  (glob_constraint, string) Result.result

val glob_constraint_to_yojson : glob_constraint -> Yojson.Safe.t

type existential_name = Glob_term.existential_name

type cases_pattern = Glob_term.cases_pattern

type glob_constr = Glob_term.glob_constr

and glob_decl = Glob_term.glob_decl

and predicate_pattern = Glob_term.predicate_pattern

and tomatch_tuple = Glob_term.tomatch_tuple

and tomatch_tuples = Glob_term.tomatch_tuples

and cases_clause = Glob_term.cases_clause

and cases_clauses = Glob_term.cases_clauses

val existential_name_of_sexp : Sexplib.Sexp.t -> Glob_term.existential_name

val sexp_of_existential_name : Glob_term.existential_name -> Sexplib.Sexp.t

val existential_name_of_yojson : 
  Yojson.Safe.t ->
  (existential_name, string) Result.result

val existential_name_to_yojson : existential_name -> Yojson.Safe.t

val cases_pattern_of_sexp : Sexplib.Sexp.t -> cases_pattern

val sexp_of_cases_pattern : cases_pattern -> Sexplib.Sexp.t

val glob_constr_of_sexp : Sexplib.Sexp.t -> glob_constr

val sexp_of_glob_constr : glob_constr -> Sexplib.Sexp.t

val glob_decl_of_sexp : Sexplib.Sexp.t -> glob_decl

val sexp_of_glob_decl : glob_decl -> Sexplib.Sexp.t

val predicate_pattern_of_sexp : Sexplib.Sexp.t -> predicate_pattern

val sexp_of_predicate_pattern : predicate_pattern -> Sexplib.Sexp.t

val tomatch_tuple_of_sexp : Sexplib.Sexp.t -> tomatch_tuple

val sexp_of_tomatch_tuple : tomatch_tuple -> Sexplib.Sexp.t

val tomatch_tuples_of_sexp : Sexplib.Sexp.t -> tomatch_tuples

val sexp_of_tomatch_tuples : tomatch_tuples -> Sexplib.Sexp.t

val cases_clause_of_sexp : Sexplib.Sexp.t -> cases_clause

val sexp_of_cases_clause : cases_clause -> Sexplib.Sexp.t

val cases_clauses_of_sexp : Sexplib.Sexp.t -> cases_clauses

val sexp_of_cases_clauses : cases_clauses -> Sexplib.Sexp.t