package coq-serapi

You can search for identifiers within the package.

in-package search v0.2.0

package coq-serapi

coq-serapi
- Library coq-serapi.coq
  - Coq
    
    Loader
- Library coq-serapi.serapi_v8_14
  - Serapi
    
    Serapi_assumptions
    
    Serapi_doc
    
    Serapi_goals
    
    Serapi_paths
    
    Serapi_pp
    
    Serapi_protocol
    
    QueryUtil
    
    ExnInfo
    
    State
- Library coq-serapi.serlib
  - Serlib
    
    SerType
    
    SJHC
    
    SJHC1
    
    Bijectable
    
    Biject
    
    Bijectable1
    
    Biject1
    
    Pierceable
    
    Pierceable1
    
    Pierce
    
    Pierce1
    
    OpaqueDesc
    
    Opaque
    
    OpaqueDesc1
    
    Opaque1
    
    Ser_attributes
    
    CAst
    
    Ser_cAst
    
    Ser_cEphemeron
    
    EBiject
    
    B
    
    Ser_cMap
    
    ExtS
    
    Make
    
    Ser_cPrimitives
    
    UVars
    
    PTP
    
    Prim_type_
    
    OOTP
    
    Op_or_type_
    
    Ser_cSet
    
    ExtS
    
    Make
    
    Ser_cUnix
    
    Ser_class_tactics
    
    Ser_constr
    
    Ser_constr_matching
    
    Ser_constrexpr
    
    Ser_context
    
    Rel
    
    Declaration
    
    Named
    
    Declaration
    
    Compacted
    
    Declaration
    
    Ser_conv_oracle
    
    Ser_cooking
    
    Ser_dAst
    
    Ser_declarations
    
    Ser_declaremods
    
    Ser_decls
    
    Ser_deprecation
    
    Ser_eConstr
    
    ERelevance
    
    Ser_entries
    
    Stateid
    
    Future
    
    Names
    
    Univ
    
    UVars
    
    Constr
    
    Declarations
    
    CPrimitives
    
    Ser_environ
    
    Ser_equality
    
    Ser_evaluable
    
    Names
    
    Ser_evar
    
    Self
    
    Set
    
    Ser_evar_kinds
    
    Ser_evd
    
    Ser_extend
    
    Ser_feedback
    
    Ser_flags
    
    Ser_float64
    
    PierceSpec
    
    Ser_future
    
    Ser_genarg
    
    GenSer0
    
    GS0
    
    GSV
    
    GenSer
    
    GS
    
    Ser_genintern
    
    Store
    
    Ser_geninterp
    
    Val
    
    Ser_genredexpr
    
    Ser_glob_term
    
    Ser_globnames
    
    Names
    
    Ser_goal_select
    
    Names
    
    Ser_goptions
    
    Ser_gramlib
    
    Gramext
    
    Ser_hints
    
    Ser_impargs
    
    Ser_int
    
    Ser_inv
    
    Ser_lib
    
    Nametab
    
    Libobject
    
    Summary
    
    Ser_libnames
    
    Ser_libobject
    
    Names
    
    Mod_subst
    
    CString
    
    Pred
    
    Dyn
    
    Reified
    
    Ser_loadpath
    
    Names
    
    Ser_loc
    
    Ser_locality
    
    Ser_locus
    
    Ser_ltac_pretype
    
    Ser_mod_subst
    
    Ser_namegen
    
    Names
    
    Ser_names
    
    Id
    
    Set
    
    Map
    
    Name
    
    DirPath
    
    DPmap
    
    Label
    
    MBId
    
    ModPath
    
    MPmap
    
    KerName
    
    KNmap
    
    Constant
    
    Cset_env
    
    Cmap
    
    Cmap_env
    
    MutInd
    
    Mindmap
    
    Mindmap_env
    
    Indset_env
    
    Indmap_env
    
    Projection
    
    Repr
    
    GlobRef
    
    Ser_nametab
    
    Ser_nativevalues
    
    Names
    
    Evar
    
    Sorts
    
    Constr
    
    Univ
    
    UVars
    
    NVI
    
    Ser_notation
    
    Ser_notation_gram
    
    Ser_notation_term
    
    Ser_notationextern
    
    Constrexpr
    
    Ser_numTok
    
    Unsigned
    
    PierceSpec
    
    UnsignedNat
    
    USNBij
    
    Signed
    
    Ser_opaqueproof
    
    Ser_pattern
    
    Ser_pp
    
    Ser_ppextend
    
    Ser_pretype_errors
    
    Ser_printer
    
    Names
    
    Ser_profile_tactic
    
    Ser_proof_bullet
    
    Ser_pstring
    
    StrSpec
    
    Ser_range
    
    Ser_reduction
    
    Ser_retroknowledge
    
    Ser_rtree
    
    RTreePierce
    
    Ser_sList
    
    SL
    
    Ser_safe_typing
    
    Ser_sorts
    
    QVar
    
    Set
    
    Quality
    
    Set
    
    QConstraints
    
    Ser_stateid
    
    Ser_stdarg
    
    Ser_stdlib
    
    Lazy
    
    List
    
    Option
    
    Ser_summary
    
    Interp
    
    Ser_tactics
    
    Ser_tactypes
    
    CAst
    
    Names
    
    Namegen
    
    EConstr
    
    DO
    
    B
    
    Ser_tok
    
    Ser_type_errors
    
    Ser_typeclasses
    
    Ser_uGraph
    
    Bound
    
    Ser_uState
    
    Ser_uint63
    
    Ser_univ
    
    Level
    
    Universe
    
    Constraints
    
    ContextSet
    
    Ser_univNames
    
    Names
    
    Ser_universes
    
    Ser_util
    
    Empty
    
    Ser_uvars
    
    Variance
    
    Instance
    
    UContext
    
    AbstractContext
    
    Ser_vernacexpr
    
    Ser_vernacextend
    
    Names
    
    Ser_vmbytecodes
    
    Names
    
    Evar
    
    Ser_vmemitcodes
    
    Ser_vmlibrary
    
    Ser_vmvalues
    
    Ser_xml_datatype
    
    Serlib_base
    
    Serlib_init
- Library coq-serapi.serlib_extra
  - Serlib_extra
    
    Ser_coqargs
    
    Names
    
    Lib
    
    Ser_stm
    
    Ser_xml_datatype
- Library coq-serapi.sertop_v8_12
  - Sertop
    
    Comp_common
    
    Js_sexp_printer
    
    Ser_version
    
    Sercomp_stats
    
    Sertop_arg
    
    Sertop_init
    
    Sertop_ser
    
    Sertop_sexp
    
    Sertop_util
- Library serlib_btauto
  - Serlib_btauto
- Library serlib_cc
  - Serlib_cc
- Library serlib_extraction
  - Serlib_extraction
    
    Ser_g_extraction
    
    Names
    
    Extraction_plugin
    
    G_extraction
    
    Table
    
    WitII
    
    WitL
    
    WitMN
- Library serlib_firstorder
  - Serlib_firstorder
    
    Ser_g_ground
    
    Loc
    
    Names
    
    Libnames
    
    Locus
- Library serlib_funind
  - Serlib_funind
    
    Ser_g_indfun
    
    CAst
    
    Names
    
    Sorts
    
    Libnames
    
    Constrexpr
    
    Tactypes
    
    Genintern
    
    EConstr
    
    Tacexpr
    
    A1
    
    WitFI
    
    WitFS
    
    Loc
    
    Vernacexpr
    
    WFFD
    
    WAU
- Library serlib_ltac
  - Serlib_ltac
    
    Ser_rewrite
    
    Ser_tacarg
    
    Ser_tacentries
    
    Ser_tacenv
    
    Ser_tacexpr
- Library serlib_ltac2
  - Serlib_ltac2
    
    Ser_g_ltac2
    
    Tac2expr
    
    L2Entry
    
    L2Expr
    
    Ser_tac2env
    
    Util
    
    Loc
    
    CAst
    
    Names
    
    Tac2expr
    
    WL2in1
    
    WL2in1V
    
    WLC2
    
    WLQ2
    
    WLV2
    
    Ser_tac2expr
    
    Loc
    
    CAst
    
    Names
    
    Libnames
    
    ObjS
    
    Obj
    
    GT2ESpec
    
    GT2E
    
    T2ESpec
    
    T2E
    
    Ser_tac2quote
- Library serlib_micromega
  - Serlib_micromega
- Library serlib_micromega_core
  - Serlib_micromega_core
- Library serlib_number_string_notation_plugin
  - Serlib_number_string_notation_plugin
    
    Ser_g_number_syntax
    
    Libnames
    
    Notation
    
    A2
    
    A3
    
    A4
    
    A5
    
    A6
    
    Ser_number_string
    
    Libnames
    
    Notation
- Library serlib_ring
  - Serlib_ring
    
    Ser_g_ring
    
    CAst
    
    Libnames
    
    Constrexpr
    
    Tactypes
    
    Genintern
    
    EConstr
    
    Tacexpr
    
    Ltac_plugin
    
    Tacexpr
    
    A0
    
    A1
    
    A2
    
    A3
- Library serlib_ssr
  - Serlib_ssr
    
    Ser_ssrast
    
    Loc
    
    Names
    
    Locus
    
    Constrexpr
    
    Genintern
    
    Geninterp
    
    Ssrmatching_plugin
    
    Ssrmatching
    
    Ltac_plugin
    
    Tacexpr
    
    Proofview
    
    Ser_ssrequality
    
    Ssrmatching_plugin
    
    Ssrmatching
    
    Ssreflect_plugin
    
    Ssrast
    
    Ssrequality
    
    Ser_ssrparser
    
    Ssrmatching
    
    Ltac_plugin
    
    Tacexpr
    
    Ssrast
    
    Ssreflect_plugin
    
    Ssrast
    
    Ssrequality
    
    Ssrparser
    
    Ssrtacs
    
    A0
    
    A1
    
    A2
    
    A3
    
    A4
    
    A5
    
    A6
    
    A7
    
    A8
    
    A9
    
    A10
    
    A11
    
    A12
    
    A13
    
    A14
    
    Wrap_ssrast
    
    Ssreflect_plugin
    
    Ssrast
    
    Wrap
- Library serlib_ssrmatching
  - Serlib_ssrmatching
    
    Ser_ssrmatching
    
    Genintern
    
    Geninterp
- Library serlib_tauto
  - Serlib_tauto
- Library serlib_zify
  - Serlib_zify
- Sources
  - coq-serapi.coq
    
    coq.ml
    
    loader.ml
  - coq-serapi.serapi_v8_14
    
    serapi.ml
    
    serapi_assumptions.ml
    
    serapi_doc.ml
    
    serapi_goals.ml
    
    serapi_paths.ml
    
    serapi_pp.ml
    
    serapi_protocol.ml
  - coq-serapi.serlib
    
    serType.ml
    
    ser_attributes.ml
    
    ser_cAst.ml
    
    ser_cEphemeron.ml
    
    ser_cMap.ml
    
    ser_cPrimitives.ml
    
    ser_cSet.ml
    
    ser_cUnix.ml
    
    ser_class_tactics.ml
    
    ser_constr.ml
    
    ser_constr_matching.ml
    
    ser_constrexpr.ml
    
    ser_context.ml
    
    ser_conv_oracle.ml
    
    ser_cooking.ml
    
    ser_dAst.ml
    
    ser_declarations.ml
    
    ser_declaremods.ml
    
    ser_decls.ml
    
    ser_deprecation.ml
    
    ser_eConstr.ml
    
    ser_entries.ml
    
    ser_environ.ml
    
    ser_equality.ml
    
    ser_evaluable.ml
    
    ser_evar.ml
    
    ser_evar_kinds.ml
    
    ser_evd.ml
    
    ser_extend.ml
    
    ser_feedback.ml
    
    ser_flags.ml
    
    ser_float64.ml
    
    ser_future.ml
    
    ser_genarg.ml
    
    ser_genintern.ml
    
    ser_geninterp.ml
    
    ser_genredexpr.ml
    
    ser_glob_term.ml
    
    ser_globnames.ml
    
    ser_goal_select.ml
    
    ser_goptions.ml
    
    ser_gramlib.ml
    
    ser_hints.ml
    
    ser_impargs.ml
    
    ser_int.ml
    
    ser_inv.ml
    
    ser_lib.ml
    
    ser_libnames.ml
    
    ser_libobject.ml
    
    ser_loadpath.ml
    
    ser_loc.ml
    
    ser_locality.ml
    
    ser_locus.ml
    
    ser_ltac_pretype.ml
    
    ser_mod_subst.ml
    
    ser_namegen.ml
    
    ser_names.ml
    
    ser_nametab.ml
    
    ser_nativevalues.ml
    
    ser_notation.ml
    
    ser_notation_gram.ml
    
    ser_notation_term.ml
    
    ser_notationextern.ml
    
    ser_numTok.ml
    
    ser_opaqueproof.ml
    
    ser_pattern.ml
    
    ser_pp.ml
    
    ser_ppextend.ml
    
    ser_pretype_errors.ml
    
    ser_printer.ml
    
    ser_profile_tactic.ml
    
    ser_proof_bullet.ml
    
    ser_pstring.ml
    
    ser_range.ml
    
    ser_reduction.ml
    
    ser_retroknowledge.ml
    
    ser_rtree.ml
    
    ser_sList.ml
    
    ser_safe_typing.ml
    
    ser_sorts.ml
    
    ser_stateid.ml
    
    ser_stdarg.ml
    
    ser_stdlib.ml
    
    ser_summary.ml
    
    ser_tactics.ml
    
    ser_tactypes.ml
    
    ser_tok.ml
    
    ser_type_errors.ml
    
    ser_typeclasses.ml
    
    ser_uGraph.ml
    
    ser_uState.ml
    
    ser_uint63.ml
    
    ser_univ.ml
    
    ser_univNames.ml
    
    ser_universes.ml
    
    ser_util.ml
    
    ser_uvars.ml
    
    ser_vernacexpr.ml
    
    ser_vernacextend.ml
    
    ser_vmbytecodes.ml
    
    ser_vmemitcodes.ml
    
    ser_vmlibrary.ml
    
    ser_vmvalues.ml
    
    ser_xml_datatype.ml
    
    serlib.ml
    
    serlib_base.ml
    
    serlib_init.ml
  - coq-serapi.serlib_extra
    
    ser_coqargs.ml
    
    ser_stm.ml
    
    ser_xml_datatype.ml
    
    serlib_extra.ml
  - coq-serapi.sertop_v8_12
    
    comp_common.ml
    
    js_sexp_printer.ml
    
    ser_version.ml
    
    sercomp_stats.ml
    
    sertop.ml
    
    sertop_arg.ml
    
    sertop_init.ml
    
    sertop_ser.ml
    
    sertop_sexp.ml
    
    sertop_util.ml
  - serlib_btauto
    
    serlib_btauto.ml
  - serlib_cc
    
    serlib_cc.ml
  - serlib_extraction
    
    ser_g_extraction.ml
    
    serlib_extraction.ml
  - serlib_firstorder
    
    ser_g_ground.ml
    
    serlib_firstorder.ml
  - serlib_funind
    
    ser_g_indfun.ml
    
    serlib_funind.ml
  - serlib_ltac
    
    ser_rewrite.ml
    
    ser_tacarg.ml
    
    ser_tacentries.ml
    
    ser_tacenv.ml
    
    ser_tacexpr.ml
    
    serlib_ltac.ml
  - serlib_ltac2
    
    ser_g_ltac2.ml
    
    ser_tac2env.ml
    
    ser_tac2expr.ml
    
    ser_tac2quote.ml
    
    serlib_ltac2.ml
  - serlib_micromega
    
    serlib_micromega.ml
  - serlib_micromega_core
    
    serlib_micromega_core.ml
  - serlib_number_string_notation_plugin
    
    ser_g_number_syntax.ml
    
    ser_number_string.ml
    
    serlib_number_string_notation_plugin.ml
  - serlib_ring
    
    ser_g_ring.ml
    
    serlib_ring.ml
  - serlib_ssr
    
    ser_ssrast.ml
    
    ser_ssrequality.ml
    
    ser_ssrparser.ml
    
    serlib_ssr.ml
    
    wrap_ssrast.ml
  - serlib_ssrmatching
    
    ser_ssrmatching.ml
    
    serlib_ssrmatching.ml
  - serlib_tauto
    
    serlib_tauto.ml
  - serlib_zify
    
    serlib_zify.ml

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Sertop`Source

Sourcemodule Comp_common : sig ... end

Sourcemodule Js_sexp_printer : sig ... end

Emilio J. Gallego Arias: Code below is adapted from Jane Street's sexplib, licence is:

Sourcemodule Ser_version : sig ... end

Sourcemodule Sercomp_stats : sig ... end

Sourcemodule Sertop_arg : sig ... end

Sourcemodule Sertop_init : sig ... end

Sourcemodule Sertop_ser : sig ... end

Sourcemodule Sertop_sexp : sig ... end

Sourcemodule Sertop_util : sig ... end

package coq-serapi

Module SertopSource

Module `Sertop`Source