package coq-serapi

You can search for identifiers within the package.

in-package search v0.2.0

coq-serapi
- Library coq-serapi.serapi_v8_11
  - Serapi
    
    Serapi_assumptions
    
    Serapi_goals
    
    Serapi_paths
    
    Serapi_pp
    
    Serapi_protocol
    
    ExnInfo
- Library coq-serapi.serlib
  - Serlib
    
    SerType
    
    S
    
    SJ
    
    S1
    
    SJ1
    
    Ser_attributes
    
    Ser_bigint
    
    Ser_cAst
    
    Ser_cEphemeron
    
    Ser_cMap
    
    ExtS
    
    Make
    
    Ser_cPrimitives
    
    Ser_cSet
    
    ExtS
    
    Make
    
    ExtSJ
    
    MakeJ
    
    Ser_cemitcodes
    
    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
    
    Ser_entries
    
    Stateid
    
    Future
    
    Names
    
    Univ
    
    Constr
    
    Declarations
    
    CPrimitives
    
    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
    
    Ser_geninterp
    
    Val
    
    Ser_genredexpr
    
    Ser_glob_term
    
    Ser_globnames
    
    Names
    
    Ser_goal
    
    Ser_goal_select
    
    Names
    
    Ser_goptions
    
    Ser_gramlib
    
    Gramext
    
    Ser_hints
    
    Ser_impargs
    
    Ser_int
    
    Ser_inv
    
    Ser_libnames
    
    Ser_loadpath
    
    Names
    
    Ser_loc
    
    Ser_locus
    
    Ser_ltac_pretype
    
    Ser_mod_subst
    
    Ser_namegen
    
    Names
    
    Ser_names
    
    Id
    
    Set
    
    Map
    
    Name
    
    DirPath
    
    DPmap
    
    Label
    
    MBId
    
    ModPath
    
    MPmap
    
    KerName
    
    Constant
    
    Cmap
    
    Cmap_env
    
    MutInd
    
    Mindmap
    
    Mindmap_env
    
    Projection
    
    Repr
    
    GlobRef
    
    Ser_nametab
    
    Ser_nativevalues
    
    Names
    
    Evar
    
    Sorts
    
    Constr
    
    Univ
    
    Ser_notation
    
    Ser_notation_gram
    
    Ser_notation_term
    
    Ser_numTok
    
    Ser_opaqueproof
    
    Ser_pattern
    
    Ser_pp
    
    Ser_ppextend
    
    Ser_pretype_errors
    
    Ser_printer
    
    Names
    
    Ser_proof
    
    Ser_proof_bullet
    
    Ser_proof_global
    
    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
    
    CAst
    
    Names
    
    Namegen
    
    EConstr
    
    Ser_tok
    
    Ser_type_errors
    
    Ser_typeclasses
    
    Ser_uGraph
    
    Ser_uState
    
    Ser_uint63
    
    Ser_univ
    
    Level
    
    Universe
    
    Variance
    
    Instance
    
    Constraint
    
    UContext
    
    AUContext
    
    ContextSet
    
    Ser_univNames
    
    Names
    
    Ser_universes
    
    Ser_util
    
    Ser_vernacexpr
    
    Ser_vernacextend
    
    Names
    
    Ser_vmvalues
    
    Ser_xml_datatype
    
    Serlib_base
    
    Serlib_init
- Library coq-serapi.sertop_v8_11
  - Sertop
    
    Ser_version
    
    Sercomp_stats
    
    Sertop_arg
    
    Sertop_init
    
    Sertop_loader
    
    Sertop_ser
    
    Sertop_sexp
    
    Sertop_util
- Library serlib_extraction
  - Serlib_extraction
    
    Ser_g_extraction
- Library serlib_firstorder
  - Serlib_firstorder
    
    Ser_g_ground
    
    Loc
    
    Names
    
    Libnames
    
    Locus
- Library serlib_funind
  - Serlib_funind
    
    Ser_g_indfun
    
    CAst
    
    Constrexpr
    
    Tactypes
    
    Genintern
    
    EConstr
    
    Tacexpr
    
    A1
    
    A2
    
    Loc
    
    Vernacexpr
- Library serlib_ltac
  - Serlib_ltac
    
    Ser_profile_ltac
    
    Ser_rewrite
    
    Ser_tacarg
    
    Ser_tacentries
    
    Ser_tacenv
    
    Ser_tacexpr
- Library serlib_setoid_ring
  - Serlib_setoid_ring
    
    Ser_g_newring
    
    CAst
    
    Libnames
    
    Constrexpr
    
    Tactypes
    
    Genintern
    
    EConstr
    
    Tacexpr
    
    Ltac_plugin
    
    Tacexpr
- 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
    
    A1
    
    A2
    
    A3
    
    A4
    
    A5
    
    A6
    
    A7
    
    A8
    
    A9
    
    A10
    
    A11
    
    A12
    
    Wrap_ssrast
    
    Ssreflect_plugin
    
    Ssrast
    
    Wrap
- Library serlib_ssrmatching
  - Serlib_ssrmatching
    
    Ser_ssrmatching
- Sources
  - coq-serapi.serapi_v8_11
    
    serapi.ml
    
    serapi_assumptions.ml
    
    serapi_goals.ml
    
    serapi_paths.ml
    
    serapi_pp.ml
    
    serapi_protocol.ml
  - coq-serapi.serlib
    
    serType.ml
    
    ser_attributes.ml
    
    ser_bigint.ml
    
    ser_cAst.ml
    
    ser_cEphemeron.ml
    
    ser_cMap.ml
    
    ser_cPrimitives.ml
    
    ser_cSet.ml
    
    ser_cemitcodes.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_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.ml
    
    ser_goal_select.ml
    
    ser_goptions.ml
    
    ser_gramlib.ml
    
    ser_hints.ml
    
    ser_impargs.ml
    
    ser_int.ml
    
    ser_inv.ml
    
    ser_libnames.ml
    
    ser_loadpath.ml
    
    ser_loc.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_numTok.ml
    
    ser_opaqueproof.ml
    
    ser_pattern.ml
    
    ser_pp.ml
    
    ser_ppextend.ml
    
    ser_pretype_errors.ml
    
    ser_printer.ml
    
    ser_proof.ml
    
    ser_proof_bullet.ml
    
    ser_proof_global.ml
    
    ser_range.ml
    
    ser_reduction.ml
    
    ser_retroknowledge.ml
    
    ser_rtree.ml
    
    ser_safe_typing.ml
    
    ser_sorts.ml
    
    ser_stateid.ml
    
    ser_stdarg.ml
    
    ser_stdlib.ml
    
    ser_stm.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_vernacexpr.ml
    
    ser_vernacextend.ml
    
    ser_vmvalues.ml
    
    ser_xml_datatype.ml
    
    serlib.ml
    
    serlib_base.ml
    
    serlib_init.ml
  - coq-serapi.sertop_v8_11
    
    ser_version.ml
    
    sercomp_stats.ml
    
    sertop.ml
    
    sertop_arg.ml
    
    sertop_init.ml
    
    sertop_loader.ml
    
    sertop_ser.ml
    
    sertop_sexp.ml
    
    sertop_util.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_profile_ltac.ml
    
    ser_rewrite.ml
    
    ser_tacarg.ml
    
    ser_tacentries.ml
    
    ser_tacenv.ml
    
    ser_tacexpr.ml
    
    serlib_ltac.ml
  - serlib_setoid_ring
    
    ser_g_newring.ml
    
    serlib_setoid_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

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

Source file `ser_equality.ml`

1
2
3
4
5
open Sexplib.Conv

type multi =
  [%import: Equality.multi]
  [@@deriving sexp]

package coq-serapi

Source file ser_equality.ml

Source file `ser_equality.ml`