package coq-serapi

You can search for identifiers within the package.

in-package search v0.2.0

package coq-serapi

coq-serapi.serapi_v8_14
- Serapi
coq-serapi.serlib
- Serlib
  - SerType
    
    Biject
    
    M
    
    Biject1
    
    M
    
    Bijectable
    
    Bijectable1
    
    Opaque
    
    M
    
    Opaque1
    
    M
    
    OpaqueDesc
    
    OpaqueDesc1
    
    Pierce
    
    M
    
    Pierce1
    
    M
    
    Pierceable
    
    Pierceable1
    
    SJHC
    
    SJHC1
  - Ser_attributes
  - Ser_cAst
  - Ser_cEphemeron
    
    B
    
    EBiject
  - Ser_cMap
    
    ExtS
    
    Make
    
    M
    
    S
  - Ser_cPrimitives
  - Ser_cSet
    
    ExtS
    
    Make
    
    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_coqargs
  - 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
    
    PierceSpec
  - Ser_future
  - Ser_genarg
    
    GS
    
    M
    
    GS0
    
    M
    
    GenSer
    
    GenSer0
  - 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
    
    KNmap
    
    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
    
    PierceSpec
    
    UnsignedNat
    
    USNBij
  - 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
    
    RTreePierce
  - Ser_safe_typing
  - Ser_sorts
  - Ser_stateid
  - Ser_stdarg
  - Ser_stdlib
    
    Lazy
  - Ser_stm
  - Ser_tacred
  - Ser_tactics
  - Ser_tactypes
    
    B
    
    DO
  - Ser_tok
  - Ser_type_errors
  - Ser_typeclasses
  - Ser_uGraph
    
    Bound
  - Ser_uState
  - Ser_uint63
  - Ser_univ
    
    AbstractContext
    
    Constraints
    
    ContextSet
    
    Instance
    
    Level
    
    UContext
    
    Universe
    
    Variance
  - Ser_univNames
  - Ser_universes
  - Ser_util
    
    Empty
  - Ser_vernacexpr
  - Ser_vernacextend
  - Ser_vmbytecodes
  - Ser_vmemitcodes
  - Ser_vmvalues
  - Ser_xml_datatype
  - Serlib_base
  - Serlib_init
coq-serapi.serlib.cc_plugin
- Serlib_cc
coq-serapi.serlib.extraction_plugin
- Serlib_extraction
  - Ser_g_extraction
coq-serapi.serlib.firstorder_plugin
- Serlib_firstorder
  - Ser_g_ground
coq-serapi.serlib.funind_plugin
- Serlib_funind
  - Ser_g_indfun
    
    A1
    
    WAU
    
    WFFD
    
    WitFI
    
    WitFS
coq-serapi.serlib.ltac
- Serlib_ltac
coq-serapi.serlib.ltac2_plugin
- Serlib_ltac2
  - Ser_g_ltac2
    
    L2Entry
    
    L2Expr
  - Ser_tac2env
    
    WL2
    
    WLC2
    
    WLQ2
    
    WLV2
  - Ser_tac2expr
    
    GT2E
    
    GT2ESpec
    
    Obj
    
    ObjS
    
    T2E
    
    T2ESpec
  - Ser_tac2quote
coq-serapi.serlib.micromega_plugin
- Serlib_micromega
coq-serapi.serlib.number_string_notation_plugin
- Serlib_number_string_notation_plugin
  - Ser_g_number_syntax
    
    A1
    
    A2
    
    A3
    
    A4
    
    A5
    
    A6
  - Ser_number
coq-serapi.serlib.ring_plugin
- Serlib_ring
  - Ser_g_ring
    
    A0
    
    A1
    
    A2
    
    A3
    
    Ltac_plugin
coq-serapi.serlib.ssreflect_plugin
- Serlib_ssr
  - Ser_ssrast
    
    Ltac_plugin
    
    Proofview
    
    Ssrmatching_plugin
  - Ser_ssrequality
    
    Ssreflect_plugin
    
    Ssrmatching_plugin
  - Ser_ssrparser
    
    A0
    
    A1
    
    A10
    
    A11
    
    A12
    
    A13
    
    A14
    
    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
    
    B_
    
    PierceRPattern
coq-serapi.serlib.tauto_plugin
- Serlib_tauto
coq-serapi.serlib.zify_plugin
- Serlib_zify
coq-serapi.sertop_v8_12
- Sertop

Legend:
Library
Module
Module type
Parameter
Class
Class type

module Ssrmatching = Serlib_ssrmatching.Ser_ssrmatching

module Ltac_plugin : sig ... end

module Ssrast = Ser_ssrast

module Ssreflect_plugin : sig ... end

type t_movearg = Ssrmatching.cpattern Ssrast.ssragens Ssrast.ssrmovearg

val t_movearg_of_sexp : Sexplib0.Sexp.t -> t_movearg

val sexp_of_t_movearg : t_movearg -> Sexplib0.Sexp.t

val t_movearg_to_yojson : t_movearg -> Yojson.Safe.t

val t_movearg_of_yojson : 
  Yojson.Safe.t ->
  t_movearg Ppx_deriving_yojson_runtime.error_or

val hash_fold_t_movearg : 
  Ppx_hash_lib.Std.Hash.state ->
  t_movearg ->
  Ppx_hash_lib.Std.Hash.state

val hash_t_movearg : t_movearg -> Ppx_hash_lib.Std.Hash.hash_value

val compare_t_movearg : t_movearg -> t_movearg -> int

val ser_wit_ssrmovearg : 
  (t_movearg, t_movearg, t_movearg) Serlib.Ser_genarg.gen_ser

val ser_wit_ssrapplyarg : 
  (Ssrast.ssrapplyarg, Ssrast.ssrapplyarg, Ssrast.ssrapplyarg)
    Serlib.Ser_genarg.gen_ser

val ser_wit_clauses : 
  (Ssrast.clauses, Ssrast.clauses, Ssrast.clauses) Serlib.Ser_genarg.gen_ser

type t_rwarg = Ssreflect_plugin.Ssrequality.ssrrwarg list

val t_rwarg_of_sexp : Sexplib0.Sexp.t -> t_rwarg

val sexp_of_t_rwarg : t_rwarg -> Sexplib0.Sexp.t

val hash_fold_t_rwarg : 
  Ppx_hash_lib.Std.Hash.state ->
  t_rwarg ->
  Ppx_hash_lib.Std.Hash.state

val hash_t_rwarg : t_rwarg -> Ppx_hash_lib.Std.Hash.hash_value

val compare_t_rwarg : t_rwarg -> t_rwarg -> int

val ser_wit_ssrrwargs : (t_rwarg, t_rwarg, t_rwarg) Serlib.Ser_genarg.gen_ser

module A0 : sig ... end

val ser_wit_ssrhavefwdwbinders : 
  (A0.raw, A0.glb, A0.top) Serlib__Ser_genarg.gen_ser

type ssrfwdview = Ssreflect_plugin.Ssrast.ast_closure_term list

val ssrfwdview_of_sexp : Sexplib0.Sexp.t -> ssrfwdview

val sexp_of_ssrfwdview : ssrfwdview -> Sexplib0.Sexp.t

val ssrfwdview_to_yojson : ssrfwdview -> Yojson.Safe.t

val ssrfwdview_of_yojson : 
  Yojson.Safe.t ->
  ssrfwdview Ppx_deriving_yojson_runtime.error_or

val hash_fold_ssrfwdview : 
  Ppx_hash_lib.Std.Hash.state ->
  ssrfwdview ->
  Ppx_hash_lib.Std.Hash.state

val hash_ssrfwdview : ssrfwdview -> Ppx_hash_lib.Std.Hash.hash_value

val compare_ssrfwdview : ssrfwdview -> ssrfwdview -> int

type ssreqid = Ssreflect_plugin.Ssrast.ssripat option

val ssreqid_of_sexp : Sexplib0.Sexp.t -> ssreqid

val sexp_of_ssreqid : ssreqid -> Sexplib0.Sexp.t

val ssreqid_to_yojson : ssreqid -> Yojson.Safe.t

val ssreqid_of_yojson : 
  Yojson.Safe.t ->
  ssreqid Ppx_deriving_yojson_runtime.error_or

val hash_fold_ssreqid : 
  Ppx_hash_lib.Std.Hash.state ->
  ssreqid ->
  Ppx_hash_lib.Std.Hash.state

val hash_ssreqid : ssreqid -> Ppx_hash_lib.Std.Hash.hash_value

val compare_ssreqid : ssreqid -> ssreqid -> int

type ssrarg =
  ssrfwdview
  * (ssreqid
     * (Ssrast.Ssrmatching_plugin.Ssrmatching.cpattern
          Ssreflect_plugin.Ssrast.ssragens
        * Ssreflect_plugin.Ssrast.ssripats))

val ssrarg_of_sexp : Sexplib0.Sexp.t -> ssrarg

val sexp_of_ssrarg : ssrarg -> Sexplib0.Sexp.t

val ssrarg_to_yojson : ssrarg -> Yojson.Safe.t

val ssrarg_of_yojson : 
  Yojson.Safe.t ->
  ssrarg Ppx_deriving_yojson_runtime.error_or

val _ : Yojson.Safe.t -> ssrarg Ppx_deriving_yojson_runtime.error_or

val hash_fold_ssrarg : 
  Ppx_hash_lib.Std.Hash.state ->
  ssrarg ->
  Ppx_hash_lib.Std.Hash.state

val hash_ssrarg : ssrarg -> Ppx_hash_lib.Std.Hash.hash_value

val compare_ssrarg : ssrarg -> ssrarg -> int

val ser_wit_ssrarg : (ssrarg, ssrarg, ssrarg) Serlib.Ser_genarg.gen_ser

module A1 : sig ... end

val ser_wit_ssrhintarg : (A1.raw, A1.glb, A1.top) Serlib__Ser_genarg.gen_ser

module A2 : sig ... end

val ser_wit_ssrseqarg : (A2.raw, A2.glb, A2.top) Serlib__Ser_genarg.gen_ser

module A3 : sig ... end

val ser_wit_ssrintrosarg : (A3.raw, A3.glb, A3.top) Serlib__Ser_genarg.gen_ser

module A4 : sig ... end

val ser_wit_ssrsufffwd : (A4.raw, A4.glb, A4.top) Serlib__Ser_genarg.gen_ser

module A5 : sig ... end

val ser_wit_ssrcongrarg : (A5.t, A5.t, A5.t) Serlib__Ser_genarg.gen_ser

module A6 : sig ... end

val ser_wit_ssrdoarg : (A6.raw, A6.glb, A6.top) Serlib__Ser_genarg.gen_ser

module A7 : sig ... end

val ser_wit_ssrsetfwd : (A7.t, A7.t, A7.t) Serlib__Ser_genarg.gen_ser

module A8 : sig ... end

val ser_wit_ssrhint : (A8.raw, A8.glb, A8.top) Serlib__Ser_genarg.gen_ser

module A9 : sig ... end

val ser_wit_ssrposefwd : (A9.t, A9.t, A9.t) Serlib__Ser_genarg.gen_ser

module A10 : sig ... end

val ser_wit_ssrunlockarg : (A10.t, A10.t, A10.t) Serlib__Ser_genarg.gen_ser

module A11 : sig ... end

val ser_wit_ssrwlogfwd : (A11.t, A11.t, A11.t) Serlib__Ser_genarg.gen_ser

module A12 : sig ... end

val ser_wit_ssrfixfwd : (A12.t, A12.t, A12.t) Serlib__Ser_genarg.gen_ser

module A13 : sig ... end

val ser_wit_ssrfwd : (A13.t, A13.t, A13.t) Serlib__Ser_genarg.gen_ser

module A14 : sig ... end

val ser_wit_ssrdgens : (A14.t, A14.t, A14.t) Serlib__Ser_genarg.gen_ser

val register : unit -> unit