coq-serapi 8.9.0+0.6.0

Libraries

This package provides the following libraries (via ocamlobjinfo):

coq-serapi.serlib

Documentation:

• Ser_loc
• Ser_cAst
• Serlib_base
• Serlib_init
• Ser_xml_datatype
• Ser_vmvalues
• Ser_vernacinterp
• Ser_bigint
• Ser_int
• Ser_names
• Ser_context
• Ser_evar
• Ser_univ
• Ser_sorts
• Ser_constr
• Ser_decl_kinds
• Ser_evar_kinds
• Ser_genarg
• Ser_dAst
• Ser_libnames
• Ser_namegen
• Ser_glob_term
• Ser_notation
• Ser_conv_oracle
• Ser_declarations
• Ser_opaqueproof
• Ser_range
• Ser_retroknowledge
• Ser_uGraph
• Ser_environ
• Ser_eConstr
• Ser_pattern
• Ser_uState
• Ser_constrexpr
• Ser_declaremods
• Ser_tok
• Ser_notation_term
• Ser_extend
• Ser_flags
• Ser_locus
• Ser_util
• Ser_genredexpr
• Ser_goal_select
• Ser_goptions
• Ser_typeclasses
• Ser_hints
• Ser_proof_bullet
• Ser_proof_global
• Ser_stateid
• Ser_univNames
• Ser_universes
• Ser_vernacexpr
• Ser_type_errors
• Ser_tactypes
• Ser_tactics
• Ser_stm
• Ser_genintern
• Ser_ltac_pretype
• Ser_stdarg
• Ser_reduction
• Ser_proof
• Ser_printer
• Ser_evd
• Ser_pretype_errors
• Ser_notation_gram
• Ser_ppextend
• Ser_pp
• Ser_nametab
• Ser_mltop
• Ser_library
• Ser_inv
• Ser_impargs
• Ser_goal
• Ser_geninterp
• Ser_feedback
• Ser_equality
• Ser_constr_matching
• Ser_class_tactics

coq-serapi.serlib.ground_plugin

Documentation:

• Ser_g_ground

coq-serapi.serlib.ltac

Documentation:

• Ser_tacexpr
• Ser_tacenv
• Ser_tacentries
• Ser_rewrite
• Ser_tacarg
• Ser_profile_ltac

coq-serapi.serlib.newring_plugin

Documentation:

• Ser_g_newring

coq-serapi.serlib.recdef_plugin

Documentation:

• Ser_g_indfun