To focus the search input from anywhere on the page, press the 'S' key.
in-package search v0.1.0
Library
Module
Module type
Parameter
Class
Class type
coq-serapi 8.15.0+0.15.0
Libraries
This package provides the following libraries (via dune):
coq-serapi.serapi_v8_14
Documentation:
Serapi.Serapi_assumptions
Serapi.Serapi_doc
Serapi.Serapi_goals
Serapi.Serapi_paths
Serapi.Serapi_pp
This module includes all of sertop custom Format-based printers for Coq datatypes.Serapi.Serapi_protocol
The SerAPI Protocol
Dependencies: coq-core.stm, coq-core.plugins.ltac, sexplib
coq-serapi.serlib
Documentation:
Serlib.SerType
Serlib.Ser_attributes
Serlib.Ser_cAst
Serlib.Ser_cEphemeron
Serlib.Ser_cMap
Serlib.Ser_cPrimitives
Serlib.Ser_cSet
Serlib.Ser_cUnix
Serlib.Ser_class_tactics
Serlib.Ser_constr
Serlib.Ser_constr_matching
Serlib.Ser_constrexpr
Serlib.Ser_context
Serlib.Ser_conv_oracle
Serlib.Ser_cooking
Serlib.Ser_coqargs
Serlib.Ser_dAst
Serlib.Ser_declarations
Serlib.Ser_declaremods
Serlib.Ser_decls
Serlib.Ser_deprecation
Serlib.Ser_eConstr
Serlib.Ser_entries
Serlib.Ser_environ
Serlib.Ser_equality
Serlib.Ser_evar
Serlib.Ser_evar_kinds
Serlib.Ser_evd
Serlib.Ser_extend
Serlib.Ser_feedback
Serlib.Ser_flags
Serlib.Ser_float64
Serlib.Ser_future
Serlib.Ser_genarg
Serlib.Ser_genintern
Serlib.Ser_geninterp
Serlib.Ser_genredexpr
Serlib.Ser_glob_term
Serlib.Ser_globnames
Serlib.Ser_goal
Serlib.Ser_goal_select
Serlib.Ser_goptions
Serlib.Ser_gramlib
Serlib.Ser_hints
Serlib.Ser_impargs
Serlib.Ser_int
Serlib.Ser_inv
Serlib.Ser_libnames
Serlib.Ser_loadpath
Serlib.Ser_loc
Serlib.Ser_locality
Serlib.Ser_locus
Serlib.Ser_ltac_pretype
Serlib.Ser_mod_subst
Serlib.Ser_namegen
Serlib.Ser_names
Serlib.Ser_nametab
Serlib.Ser_nativevalues
Serlib.Ser_notation
Serlib.Ser_notation_gram
Serlib.Ser_notation_term
Serlib.Ser_numTok
Serlib.Ser_opaqueproof
Serlib.Ser_pattern
Serlib.Ser_pp
Serlib.Ser_ppextend
Serlib.Ser_pretype_errors
Serlib.Ser_printer
Serlib.Ser_proof
Serlib.Ser_proof_bullet
Serlib.Ser_range
Serlib.Ser_reduction
Serlib.Ser_retroknowledge
Serlib.Ser_rtree
Serlib.Ser_safe_typing
Serlib.Ser_sorts
Serlib.Ser_stateid
Serlib.Ser_stdarg
Serlib.Ser_stdlib
Serlib.Ser_stm
Serlib.Ser_tacred
Serlib.Ser_tactics
Serlib.Ser_tactypes
Serlib.Ser_tok
Serlib.Ser_type_errors
Serlib.Ser_typeclasses
Serlib.Ser_uGraph
Serlib.Ser_uState
Serlib.Ser_uint63
Serlib.Ser_univ
Serlib.Ser_univNames
Serlib.Ser_universes
Serlib.Ser_util
Serlib.Ser_vernacexpr
Serlib.Ser_vernacextend
Serlib.Ser_vmbytecodes
Serlib.Ser_vmemitcodes
Serlib.Ser_vmvalues
Serlib.Ser_xml_datatype
Serlib.Serlib_base
Serlib.Serlib_init
Dependencies: coq-core.stm, sexplib, ppx_sexp_conv.runtime-lib, ppx_deriving.runtime, ppx_deriving_yojson.runtime, yojson
coq-serapi.serlib.extraction_plugin
Documentation:
Dependencies: coq-core.plugins.extraction, coq-serapi.serlib, ppx_sexp_conv.runtime-lib
coq-serapi.serlib.firstorder_plugin
Documentation:
Dependencies: coq-core.plugins.firstorder, coq-serapi.serlib, sexplib, ppx_sexp_conv.runtime-lib
coq-serapi.serlib.funind_plugin
Documentation:
Dependencies: coq-core.plugins.funind, coq-serapi.serlib, coq-serapi.serlib.ltac, sexplib, ppx_sexp_conv.runtime-lib
coq-serapi.serlib.ltac
Documentation:
Serlib_ltac.Ser_profile_ltac
Serlib_ltac.Ser_rewrite
Serlib_ltac.Ser_tacarg
Serlib_ltac.Ser_tacentries
Serlib_ltac.Ser_tacenv
Serlib_ltac.Ser_tacexpr
Dependencies: coq-core.plugins.ltac, coq-serapi.serlib, sexplib, ppx_sexp_conv.runtime-lib
coq-serapi.serlib.ring_plugin
Documentation:
Dependencies: coq-core.plugins.ring, coq-serapi.serlib, coq-serapi.serlib.ltac, sexplib, ppx_sexp_conv.runtime-lib
coq-serapi.serlib.ssreflect_plugin
Documentation:
Dependencies: coq-core.plugins.ssreflect, coq-serapi.serlib, coq-serapi.serlib.ltac, coq-serapi.serlib.ssrmatching_plugin, sexplib, ppx_sexp_conv.runtime-lib
coq-serapi.serlib.ssrmatching_plugin
Documentation:
Dependencies: coq-core.plugins.ssrmatching, coq-serapi.serlib, coq-serapi.serlib.ltac, sexplib, ppx_sexp_conv.runtime-lib
coq-serapi.sertop_v8_12
Documentation:
Sertop.Ser_version
Sertop.Sercomp_stats
Sertop.Sertop_arg
Sertop.Sertop_init
Sertop.Sertop_loader
Sertop.Sertop_ser
Sertop.Sertop_sexp
Sertop.Sertop_util
Dependencies: findlib.dynload, cmdliner, coq-serapi.serapi_v8_14, coq-serapi.serlib, coq-serapi.serlib.ltac, ppx_sexp_conv.runtime-lib