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:

• Serlib_extraction.Ser_g_extraction

Dependencies: coq-core.plugins.extraction, coq-serapi.serlib, ppx_sexp_conv.runtime-lib

coq-serapi.serlib.firstorder_plugin

Documentation:

• Serlib_firstorder.Ser_g_ground

Dependencies: coq-core.plugins.firstorder, coq-serapi.serlib, sexplib, ppx_sexp_conv.runtime-lib

coq-serapi.serlib.funind_plugin

Documentation:

• Serlib_funind.Ser_g_indfun

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:

• Serlib_ring.Ser_g_ring

Dependencies: coq-core.plugins.ring, coq-serapi.serlib, coq-serapi.serlib.ltac, sexplib, ppx_sexp_conv.runtime-lib

coq-serapi.serlib.ssreflect_plugin

Documentation:

• Serlib_ssr.Ser_ssrast
• Serlib_ssr.Ser_ssrequality
• Serlib_ssr.Ser_ssrparser
• Serlib_ssr.Wrap_ssrast

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:

• Serlib_ssrmatching.Ser_ssrmatching

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