package coq-serapi

You can search for identifiers within the package.

in-package search v0.2.0

package coq-serapi

coq-serapi.serapi_v8_10
coq-serapi.serlib
- Serlib
  - SerType
    
    S
    
    S1
    
    SJ
    
    SJ1
  - Ser_attributes
  - Ser_bigint
  - Ser_cAst
  - Ser_cEphemeron
  - Ser_cMap
    
    ExtS
    
    Make
    
    M
    
    S
  - Ser_cPrimitives
  - Ser_cSet
    
    ExtS
    
    ExtSJ
    
    Make
    
    M
    
    S
    
    MakeJ
    
    M
    
    S
  - Ser_cemitcodes
  - 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_decl_kinds
  - Ser_declarations
  - Ser_declaremods
  - Ser_eConstr
  - Ser_entries
  - Ser_environ
  - Ser_equality
  - Ser_evar
    
    Self
    
    Set
  - Ser_evar_kinds
  - Ser_evd
  - Ser_extend
  - Ser_feedback
  - Ser_flags
  - Ser_future
  - Ser_genarg
  - Ser_genintern
  - 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_library
  - Ser_loc
  - Ser_locus
  - Ser_ltac_pretype
  - Ser_mltop
  - Ser_mod_subst
  - Ser_namegen
  - Ser_names
    
    Cmap
    
    Cmap_env
    
    Constant
    
    DirPath
    
    GlobRef
    
    Id
    
    Map
    
    Set
    
    KerName
    
    Label
    
    MBId
    
    MPmap
    
    Mindmap
    
    Mindmap_env
    
    ModPath
    
    MutInd
    
    Name
    
    Projection
    
    Repr
  - Ser_nametab
  - Ser_notation
  - Ser_notation_gram
  - Ser_notation_term
  - Ser_numTok
  - Ser_opaqueproof
  - Ser_pattern
  - Ser_pp
  - Ser_ppextend
  - Ser_pretype_errors
  - Ser_printer
  - 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
  - Ser_tok
  - Ser_type_errors
  - Ser_typeclasses
  - Ser_uGraph
  - 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_vmvalues
  - Ser_xml_datatype
  - Serlib_base
  - Serlib_init
coq-serapi.serlib.extraction_plugin
- Ser_g_extraction
coq-serapi.serlib.ground_plugin
- Ser_g_ground
coq-serapi.serlib.ltac
coq-serapi.serlib.newring_plugin
- Ser_g_newring
  - Ltac_plugin
coq-serapi.serlib.recdef_plugin
- Ser_g_indfun
  - A1
  - A2
coq-serapi.serlib.ssreflect_plugin
- Ser_ssrast
- 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
- Ser_ssrmatching
coq-serapi.sertop_v8_10

Legend:
Library
Module
Module type
Parameter
Class
Class type

type t = CPrimitives.t =

| Int63head0
| Int63tail0
| Int63add
| Int63sub
| Int63mul
| Int63div
| Int63mod
| Int63lsr
| Int63lsl
| Int63land
| Int63lor
| Int63lxor
| Int63addc
| Int63subc
| Int63addCarryC
| Int63subCarryC
| Int63mulc
| Int63diveucl
| Int63div21
| Int63addMulDiv
| Int63eq
| Int63lt
| Int63le
| Int63compare

val to_yojson : t -> Yojson.Safe.t

val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or

val t_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> t

val sexp_of_t : t -> Ppx_sexp_conv_lib.Sexp.t

type prim_type = CPrimitives.prim_type =

| PT_int63

val prim_type_to_yojson : prim_type -> Yojson.Safe.t

val prim_type_of_yojson : 
  Yojson.Safe.t ->
  prim_type Ppx_deriving_yojson_runtime.error_or

val prim_type_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> prim_type

val sexp_of_prim_type : prim_type -> Ppx_sexp_conv_lib.Sexp.t

type op_or_type = CPrimitives.op_or_type =

| OT_op of t
| OT_type of prim_type

val op_or_type_to_yojson : op_or_type -> Yojson.Safe.t

val op_or_type_of_yojson : 
  Yojson.Safe.t ->
  op_or_type Ppx_deriving_yojson_runtime.error_or

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

val op_or_type_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> op_or_type

val sexp_of_op_or_type : op_or_type -> Ppx_sexp_conv_lib.Sexp.t