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.serapi_v8_13
  - Serapi
    
    Serapi_assumptions
    
    Serapi_doc
    
    Serapi_goals
    
    Serapi_paths
    
    Serapi_pp
    
    Serapi_protocol
    
    QueryUtil
    
    ExnInfo
    
    State
- Library coq-serapi.serlib
  - Serlib
    
    SerType
    
    S
    
    SJ
    
    S1
    
    SJ1
    
    Ser_attributes
    
    Ser_cAst
    
    Ser_cEphemeron
    
    Ser_cMap
    
    ExtS
    
    Make
    
    Ser_cPrimitives
    
    Ser_cSet
    
    ExtS
    
    Make
    
    ExtSJ
    
    MakeJ
    
    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
    
    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
    
    Store
    
    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_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
    
    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
    
    Unsigned
    
    Signed
    
    Ser_opaqueproof
    
    Ser_pattern
    
    Ser_pp
    
    Ser_ppextend
    
    Ser_pretype_errors
    
    Ser_printer
    
    Names
    
    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
    
    CAst
    
    Names
    
    Namegen
    
    EConstr
    
    Ser_tok
    
    Ser_type_errors
    
    Ser_typeclasses
    
    Ser_uGraph
    
    Bound
    
    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_vmemitcodes
    
    Ser_vmvalues
    
    Ser_xml_datatype
    
    Serlib_base
    
    Serlib_init
- Library coq-serapi.sertop_v8_12
  - 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_ring
  - Serlib_ring
    
    Ser_g_ring
    
    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_13
    
    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_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_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_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_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_vmemitcodes.ml
    
    ser_vmvalues.ml
    
    ser_xml_datatype.ml
    
    serlib.ml
    
    serlib_base.ml
    
    serlib_init.ml
  - coq-serapi.sertop_v8_12
    
    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_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

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

Module `Serlib_ssr.Ser_ssrparser`Source

Sourcemodule Ssrmatching = Serlib_ssrmatching.Ser_ssrmatching

Sourcemodule Ltac_plugin : sig ... end

Sourcemodule Ssrast = Ser_ssrast

Sourcemodule Ssreflect_plugin : sig ... end

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

Sourceval t_movearg_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> t_movearg

Sourceval sexp_of_t_movearg : t_movearg -> Ppx_sexp_conv_lib.Sexp.t

Source

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

Source

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

Source

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

Sourcetype t_rwarg = Ssreflect_plugin.Ssrequality.ssrrwarg list

Sourceval t_rwarg_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> t_rwarg

Sourceval sexp_of_t_rwarg : t_rwarg -> Ppx_sexp_conv_lib.Sexp.t

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

Sourcetype t_h1 = Ssrast.Ltac_plugin.Tacexpr.raw_tactic_expr Ssrast.fwdbinders

Sourceval t_h1_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> t_h1

Sourceval sexp_of_t_h1 : t_h1 -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype t_h2 = Ssrast.Ltac_plugin.Tacexpr.glob_tactic_expr Ssrast.fwdbinders

Sourceval t_h2_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> t_h2

Sourceval sexp_of_t_h2 : t_h2 -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype t_h3 = Ssrast.Geninterp.Val.t Ssrast.fwdbinders

Sourceval t_h3_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> t_h3

Sourceval sexp_of_t_h3 : t_h3 -> Ppx_sexp_conv_lib.Sexp.t

Sourceval ser_wit_ssrhavefwdwbinders : (t_h1, t_h2, t_h3) Serlib.Ser_genarg.gen_ser

Sourcetype ssrfwdview = Ssrast.ast_closure_term list

Sourceval ssrfwdview_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrfwdview

Sourceval sexp_of_ssrfwdview : ssrfwdview -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype ssreqid = Ssrast.ssripat option

Sourceval ssreqid_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssreqid

Sourceval sexp_of_ssreqid : ssreqid -> Ppx_sexp_conv_lib.Sexp.t

Source

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

Sourceval ssrarg_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrarg

Sourceval sexp_of_ssrarg : ssrarg -> Ppx_sexp_conv_lib.Sexp.t

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

Sourcetype h_h1 = Ssrast.Ltac_plugin.Tacexpr.raw_tactic_expr Ssrast.ssrhint

Sourceval h_h1_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> h_h1

Sourceval sexp_of_h_h1 : h_h1 -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype h_h2 = Ssrast.Ltac_plugin.Tacexpr.glob_tactic_expr Ssrast.ssrhint

Sourceval h_h2_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> h_h2

Sourceval sexp_of_h_h2 : h_h2 -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype h_h3 = Ssrast.Geninterp.Val.t Ssrast.ssrhint

Sourceval h_h3_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> h_h3

Sourceval sexp_of_h_h3 : h_h3 -> Ppx_sexp_conv_lib.Sexp.t

Sourceval ser_wit_ssrhintarg : (h_h1, h_h2, h_h3) Serlib.Ser_genarg.gen_ser

Sourcemodule A1 : sig ... end

Sourceval ser_wit_ssrseqarg : (A1.h1, A1.h2, A1.h3) Serlib.Ser_genarg.gen_ser

Sourcemodule A2 : sig ... end

Sourceval ser_wit_ssrintrosarg : (A2.h1, A2.h2, A2.h3) Serlib.Ser_genarg.gen_ser

Sourcemodule A3 : sig ... end

Sourceval ser_wit_ssrsufffwd : (A3.h1, A3.h2, A3.h3) Serlib.Ser_genarg.gen_ser

Sourcemodule A4 : sig ... end

Sourceval ser_wit_ssrcongrarg : (A4.h1, A4.h1, A4.h1) Serlib.Ser_genarg.gen_ser

Sourcemodule A5 : sig ... end

Sourceval ser_wit_ssrdoarg : (A5.h1, A5.h2, A5.h3) Serlib.Ser_genarg.gen_ser

Sourcemodule A6 : sig ... end

Sourceval ser_wit_ssrsetfwd : (A6.h1, A6.h1, A6.h1) Serlib.Ser_genarg.gen_ser

Sourcemodule A7 : sig ... end

Sourceval ser_wit_ssrhint : (A7.h1, A7.h2, A7.h3) Serlib.Ser_genarg.gen_ser

Sourcemodule A8 : sig ... end

Sourceval ser_wit_ssrposefwd : (A8.h1, A8.h1, A8.h1) Serlib.Ser_genarg.gen_ser

Sourcemodule A9 : sig ... end

Sourceval ser_wit_ssrunlockarg : (A9.h1, A9.h1, A9.h1) Serlib.Ser_genarg.gen_ser

Sourcemodule A10 : sig ... end

Sourceval ser_wit_ssrwlogfwd : (A10.h1, A10.h1, A10.h1) Serlib.Ser_genarg.gen_ser

Sourcemodule A11 : sig ... end

Sourceval ser_wit_ssrfixfwd : (A11.h1, A11.h1, A11.h1) Serlib.Ser_genarg.gen_ser

Sourcemodule A12 : sig ... end

Sourceval ser_wit_ssrfwd : (A12.h1, A12.h1, A12.h1) Serlib.Ser_genarg.gen_ser

Sourceval register : unit -> unit

package coq-serapi

Module Serlib_ssr.Ser_ssrparserSource

Module `Serlib_ssr.Ser_ssrparser`Source