coq 8.9.1

Libraries

This package provides the following libraries (via ocamlobjinfo):

coq.grammar

Documentation:

• Q_util
• Argextend
• Tacextend
• Vernacextend

coq.clib

Documentation:

• CObj
• CEphemeron
• Hashset
• Hashcons
• OrderedType
• CSet
• CMap
• CList
• CString
• CStack
• Int Integer values.
• Range
• HMap
• Bigint
• CArray
• Option Option values.
• CUnix
• Segmenttree
• Unicodetable
• Unicode
• Minisys
• CThread
• Trie
• Predicate
• Heap
• Unionfind
• Dyn
• Store
• Exninfo
• Backtrace
• IStream
• Terminal
• Monad
• Diff2

coq.lib

Documentation:

• Coq_config
• Hook
• Flags
• Control
• Util
• Pp
• Pp_diff
• Stateid
• Loc
• Feedback
• CErrors
• CWarnings
• Rtree
• System
• Explore
• CProfile
• Future
• Spawn
• CAst
• DAst
• Genarg
• RemoteCounter
• Aux_file
• Envars
• CoqProject_file

coq.vm

Documentation:

coq.kernel

Documentation:

• Names
• Uint31
• Univ
• UGraph
• Esubst
• Sorts
• Evar
• Context
• Constr
• Vars
• Term
• Mod_subst
• Vmvalues
• Cbytecodes
• Copcodes
• Cemitcodes
• Opaqueproof
• Declarations
• Entries
• Nativevalues
• CPrimitives
• Declareops
• Retroknowledge
• Conv_oracle
• Environ
• CClosure
• Reduction
• Clambda
• Nativelambda
• Cbytegen
• Nativecode
• Nativelib
• Csymtable
• Vm
• Vconv
• Nativeconv
• Type_errors
• Modops
• Inductive
• Typeops
• Indtypes
• Cooking
• Term_typing
• Subtyping
• Mod_typing
• Nativelibrary
• Safe_typing

coq.library

Documentation:

• Libnames
• Globnames
• Libobject
• Summary
• Nametab
• Global
• Decl_kinds
• Lib
• Declaremods
• Loadpath
• Library
• States
• Kindops
• Dischargedhypsmap
• Goptions
• Decls
• Keys
• Coqlib

coq.engine

Documentation:

• UnivNames
• UnivGen
• UnivSubst
• UnivProblem
• UnivMinim
• Universes
• Univops
• UState
• Nameops
• Evar_kinds
• Evd
• EConstr
• Namegen
• Termops
• Evarutil
• Logic_monad
• Proofview_monad
• Proofview
• Ftactic

coq.pretyping

Documentation:

• Geninterp
• Locus
• Locusops
• Pretype_errors
• Reductionops
• Inductiveops
• InferCumulativity
• Vnorm
• Arguments_renaming
• Nativenorm
• Retyping
• Cbv
• Find_subterm
• Evardefine
• Evarsolve
• Recordops
• Heads
• Evarconv
• Typing
• Glob_term
• Ltac_pretype
• Glob_ops
• Pattern
• Patternops
• Constr_matching
• Tacred
• Typeclasses_errors
• Typeclasses
• Classops
• Program
• Coercion
• Detyping
• Indrec
• Cases
• Pretyping
• Unification

coq.interp

Documentation:

• Constrexpr
• Genredexpr
• Redops
• Tactypes
• Stdarg
• Genintern
• Notation_term
• Notation_ops
• Notation
• Syntax_def
• Smartlocate
• Constrexpr_ops
• Dumpglob
• Reserve
• Impargs
• Implicit_quantifiers
• Constrintern
• Modintern
• Constrextern
• Discharge
• Declare

coq.proofs

Documentation:

• Miscprint
• Goal
• Evar_refiner
• Proof_type
• Logic
• Refine
• Proof
• Goal_select
• Proof_bullet
• Proof_global
• Redexpr
• Refiner
• Tacmach
• Pfedit
• Clenv
• Clenvtac

coq.parsing

Documentation:

• Tok
• CLexer
• Extend
• Notation_gram
• Ppextend
• Notgram_ops
• Pcoq
• G_constr
• G_prim

coq.printing

Documentation:

• Genprint
• Pputils
• Ppconstr
• Proof_diffs
• Printer
• Printmod
• Prettyp

coq.tactics

Documentation:

• Dnet
• Dn
• Btermdn
• Tacticals
• Hipattern
• Ind_tables
• Eqschemes
• Elimschemes
• Tactics
• Elim
• Equality
• Contradiction
• Inv
• Leminv
• Hints
• Auto
• Eauto
• Class_tactics
• Term_dnet
• Eqdecide
• Autorewrite

coq.vernac

Documentation:

• Vernacexpr
• Pvernac
• G_vernac
• G_proofs
• Vernacprop
• Himsg
• ExplainErr
• Locality
• Egramml
• Vernacinterp
• Ppvernac
• Proof_using
• Lemmas
• Class
• Egramcoq
• Metasyntax
• Auto_ind_decl
• Search
• Indschemes
• DeclareDef
• Obligations
• ComDefinition
• ComAssumption
• ComInductive
• ComFixpoint
• ComProgramFixpoint
• Classes
• Record
• Assumptions
• Vernacstate
• Mltop
• Topfmt
• Vernacentries
• Misctypes

coq.stm

Documentation:

• Spawned
• Dag
• Vcs
• TQueue
• WorkerPool
• Vernac_classifier
• CoqworkmgrApi
• AsyncTaskQueue
• Stm
• ProofBlockDelimiter
• Vio_checking

coq.toplevel

Documentation:

• Vernac
• Usage
• Coqinit
• Coqargs
• G_toplevel
• Coqloop
• Coqtop
• WorkerLoop

coq.idetop

Documentation:

coq.ide

Documentation:

coq.plugins.ltac

Documentation:

coq.plugins.tauto

Documentation:

coq.plugins.omega

Documentation:

coq.plugins.romega

Documentation:

coq.plugins.micromega

Documentation:

coq.plugins.quote

Documentation:

coq.plugins.newring

Documentation:

coq.plugins.extraction

Documentation:

coq.plugins.cc

Documentation:

coq.plugins.ground

Documentation:

coq.plugins.rtauto

Documentation:

coq.plugins.btauto

Documentation:

coq.plugins.recdef

Documentation:

coq.plugins.nsatz

Documentation:

coq.plugins.natsyntax

Documentation:

coq.plugins.zsyntax

Documentation:

coq.plugins.rsyntax

Documentation:

coq.plugins.int31syntax

Documentation:

coq.plugins.asciisyntax

Documentation:

coq.plugins.stringsyntax

Documentation:

coq.plugins.derive

Documentation:

coq.plugins.ssrmatching

Documentation:

coq.plugins.ssreflect

Documentation: