The entry point of this library is the module: Boot
.
The entry point of this library is the module: Coq_checklib
.
This library exposes the following toplevel modules:
CArray
CEphemeron
CList
CMap
CObj
CSet
CSig
Missing pervasive types from OCaml stdlibCString
CThread
CUnix
Diff2
An implementation of Eugene Myers' O(ND) Difference Algorithm[1]. This implementation is a port of util.lcs module of Gauche Scheme interpreter.Dyn
Dynamically typed valuesExninfo
Additional information worn by exceptions.HMap
Hashcons
Generic hash-consing.Hashset
Adapted from Damien Doligez, projet Para, INRIA Rocquencourt, OCaml stdlib.Heap
HeapsIStream
Int
A native integer module with usual utility functions.Memprof_coq
Monad
Combinators on monadic computations.Mutex_aux
NeList
Option
Module implementing basic combinators for OCaml option type. It tries follow closely the style of OCaml standard library.OrderedType
PolyMap
Predicate
Infinite sets over a chosen OrderedType
.Range
Skewed listsSList
Sparse lists.Segmenttree
This module is a very simple implementation of "segment trees".Store
Terminal
Trie
Generic functorized trie data structure.Unicode
Unicode utilitiesUnicodetable
Unionfind
An imperative implementation of partitions via Union-FindThe entry point of this library is the module: Coq_config
.
The entry point of this library is the module: Coq_byte_config
.
The entry point of this library is the module: Coqargs
.
The entry point of this library is the module: Coqdeplib
.
The entry point of this library is the module: CoqworkmgrApi
.
The entry point of this library is the module: Debugger_support
.
This library exposes the following toplevel modules:
Top_printers
Printers for the OCaml toplevel.Vm_printers
This library exposes the following toplevel modules:
EConstr
Evar_kinds
The kinds of existential variableEvarutil
This module provides useful higher-level functions for evar manipulation.Evd
This file defines the pervasive unification state used everywhere in Coq tactic engine. It is very low-level and most of the functions exported here are irrelevant to the standard API user. Consider using Evarutil
or Proofview
instead.Ftactic
This module defines potentially focussing tactics. They are used by Ltac to emulate the historical behaviour of always-focussed tactics while still allowing to remain global when the goal is not needed.Logic_monad
This file implements the low-level monadic operations used by the tactic monad. The monad is divided into two layers: a non-logical layer which consists in operations which will not (or cannot) be backtracked in case of failure (input/output or persistent state) and a logical layer which handles backtracking, proof manipulation, and any other effect which needs to backtrack.Namegen
This file features facilities to generate fresh names.Nameops
Identifiers and namesProfile_tactic
Ltac profiling primitivesProofview
This files defines the basic mechanism of proofs: the proofview
type is the state which tactics manipulate (a global state for existential variables, together with the list of goals), and the type 'a tactic
is the (abstract) type of tactics modifying the proof state and returning a value of type 'a
.Proofview_monad
This file defines the datatypes used as internal states by the tactic monad, and specialises the Logic_monad
to these types. It should not be used directly. Consider using Proofview
instead.Termops
This file defines various utilities for term manipulation that are not needed in the kernel.UState
This file defines universe unification states which are part of evarmaps. Most of the API below is reexported in Evd
. Consider using higher-level primitives when needed.UnivFlex
UnivGen
UnivMinim
UnivNames
Local universe name <-> level mappingUnivProblem
UnivSubst
The entry point of this library is the module: Gramlib
.
This library exposes the following toplevel modules:
Abbreviation
Abbreviations.Constrexpr
Constrexpr_ops
Constrexpr_ops: utilities on constr_expr
Constrextern
Translation of pattern, cases pattern, glob_constr and term into syntax trees for printingConstrintern
Translation from front abstract syntax of term to untyped terms (glob_constr)Decls
Dumpglob
This file implements the Coq's .glob
file format, which provides information about the objects that are defined and referenced from a Coq file.Genintern
Impargs
Implicit_quantifiers
Modintern
Module internalization errorsNotation
NotationsNotation_ops
Constr default entriesNotation_term
notation_constr
Notationextern
Declaration of uninterpretation functions (i.e. printing rules) for notationsNumTok
Numbers in different forms: signed or unsigned, possibly with fractional part and exponent.Reserve
Smartlocate
locate_global_with_alias
locates global reference possibly following a notation if this notation has a role of aliasing; raise Not_found
if not bound in the global env; raise a UserError
if bound to a syntactic def that does not denote a referenceThis library exposes the following toplevel modules:
CClosure
Lazy reduction.CPrimitives
Constant_typing
Constr
This file defines the most important datatype of Coq, namely kernel terms, as well as a handful of generic manipulation functions.Context
The modules defined below represent a local context as defined by Chapter 4 in the Reference Manual:Conv_oracle
Conversion
Cooking
Declarations
This module defines the internal representation of global declarations. This includes global constants/axioms, mutual inductive definitions, modules and module typesDeclareops
Operations concerning types in Declarations
: constant_body
, mutual_inductive_body
, module_body
...Discharge
Entries
This module defines the entry types for global declarations. This information is entered in the environments. This includes global constants/axioms, mutual inductive definitions, modules and module typesEnviron
Unsafe environments. We define here a datatype for environments. Since typing is not yet defined, it is not possible to check the informations added in environments, and that is why we speak here of ``unsafe'' environments.Esubst
Explicit substitutionsEvar
This module defines existential variables, which are isomorphic to int
. Nonetheless, casting from an int
to a variable is deemed unsafe, so that to keep track of such casts, one has to use the provided unsafe_of_int
function.Float64
Float64_common
Genlambda
Intermediate language used by both the VM and native.HConstr
IndTyping
Indtypes
Inductive
InferCumulativity
Mod_subst
Mod_typing
Main functions for translating module entriesModops
Names
This file defines a lot of different notions of names used pervasively in the kernel as well as in other places. The essential datatypes exported by this API are:Nativecode
This file defines the mllambda code generation phase of the native compiler. mllambda represents a fragment of ML, and can easily be printed to OCaml code.Nativeconv
This module implements the conversion test by compiling to OCaml codeNativelambda
This file defines the lambda code generation phase of the native compilerNativelib
This file provides facilities to access OCaml compiler and dynamic linker, used by the native compiler.Nativelibrary
This file implements separate compilation for libraries in the native compilerNativevalues
This modules defines the representation of values internally used by the native compiler. Be careful when removing apparently dead code from this interface, as it may be used by programs generated at runtime.Opaqueproof
This module implements the handling of opaque proof terms. Opaque proof terms are special since:Parray
Partial_subst
Primred
Pstring
Primitive string
type.RedFlags
Delta implies all consts (both global (= by kernel_name
) and local (= by Rel
or Var
)), all evars, and letin's. Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of a LetIn expression is Letin reductionReduction
None of these functions do eta reductionRelevanceops
We can take advantage of non-cumulativity of SProp to avoid fully retyping terms when we just want to know if they inhabit some proof-irrelevant type.Retroknowledge
Rtree
Safe_typing
Section
Kernel implementation of sections.Sorts
Subtyping
Term
TransparentState
Type_errors
Type errors. \label{typeerrors}
Typeops
UGraph
UVars
Uint63
Univ
Values
Vars
Vconv
Vm
Vmbytecodes
Vmbytegen
Vmemitcodes
Vmerrors
Vmlambda
Vmlibrary
Vmopcodes
Vmsymtable
Vmvalues
ValuesThis library exposes the following toplevel modules:
AcyclicGraph
Graphs representing strict ordersAux_file
CAst
CDebug
CErrors
This modules implements basic manipulations of errors for use throughout Coq's code.CWarnings
Control
Global control of Coq.CoqProject_file
DAst
Lazy AST node wrapper. Only used for glob_constr
as of today.Deprecation
Envars
This file provides a high-level interface to the environment variables needed by Coq to run (such as coqlib). The values of these variables may come from different sources (shell environment variables, command line options, options set at the time Coq was build).Feedback
Flags
Global options of the system.Hook
This module centralizes the notions of hooks. Hooks are pointers that are to be set at runtime exactly once.Instr
Platform-specific Implementation of a global instruction counter.Loc
NewProfile
ObjFile
Pp
Coq document type.Pp_diff
Computes the differences between 2 Pp's and adds additional tags to a Pp to highlight them. Strings are split into tokens using the Coq lexer, then the lists of tokens are diffed using the Myers algorithm. A fixup routine, shorten_diff_span, shortens the span of the diff result in some cases.Quickfix
Spawn
Stateid
System
UserWarn
This is about warnings triggered from user .v code ("warn" attibute). See cWarnings.mli for the generic warning interface.Util
This module contains numerous utility functions on strings, lists, arrays, etc.Xml_datatype
This library exposes the following toplevel modules:
Coqlib
Deprecated alias for RocqlibGlobal
This module defines the global environment of Coq. The functions below are exactly the same as the ones in Safe_typing
, operating on that global environment. add_*
functions perform name verification, i.e. check that the name given as argument match those provided by Safe_typing
.Globnames
Goptions
This module manages customization parameters at the vernacular levelLib
Lib: record of operations, backtrack, low-level sectionsLibnames
Libobject
Libobject
declares persistent objects, given with methods:Library_info
Locality
* Managing localityNametab
This module contains the tables for globalization.Rocqlib
Indirection between logical names and global references.Summary
This library exposes the following toplevel modules:
CLexer
Extend
Entry keys for constr notationsG_constr
G_prim
Notation_gram
Notgram_ops
Pcoq
Deprecated alias for ProcqProcq
The parser of CoqTok
The type of token for the Coq lexer and parserThe entry point of this library is the module: Perf
.
The entry point of this library is the module: Btauto_plugin
.
The entry point of this library is the module: Cc_plugin
.
The entry point of this library is the module: Cc_core_plugin
.
The entry point of this library is the module: Derive_plugin
.
The entry point of this library is the module: Extraction_plugin
.
The entry point of this library is the module: Firstorder_plugin
.
The entry point of this library is the module: Firstorder_core_plugin
.
The entry point of this library is the module: Funind_plugin
.
The entry point of this library is the module: Ltac_plugin
.
The entry point of this library is the module: Ltac2_plugin
.
The entry point of this library is the module: Ltac2_ltac1_plugin
.
The entry point of this library is the module: Micromega_plugin
.
The entry point of this library is the module: Micromega_core_plugin
.
The entry point of this library is the module: Nsatz_plugin
.
The entry point of this library is the module: Nsatz_core_plugin
.
The entry point of this library is the module: Number_string_notation_plugin
.
The entry point of this library is the module: Ring_plugin
.
The entry point of this library is the module: Rtauto_plugin
.
The entry point of this library is the module: Ssreflect_plugin
.
The entry point of this library is the module: Ssrmatching_plugin
.
The entry point of this library is the module: Tauto_plugin
.
The entry point of this library is the module: Tuto0_plugin
.
The entry point of this library is the module: Tuto1_plugin
.
The entry point of this library is the module: Tuto2_plugin
.
The entry point of this library is the module: Tuto3_plugin
.
The entry point of this library is the module: Zify_plugin
.
This library exposes the following toplevel modules:
Arguments_renaming
Cases
Cbv
Coercion
Coercionops
Combinators
telescope env sigma ctx
turns a context x1:A1;...;xn:An
into a right-associated nested sigma-type of the right sort. It returns:Constr_matching
This module implements pattern-matching on termsDetyping
Evaluable
Evaluable references (whose transparency can be controlled)Evarconv
Evardefine
Evarsolve
Find_subterm
Finding subterms, possibly up to some unification function, possibly at some given occurrencesGenarg
Generic arguments used by the extension mechanisms of several Coq ASTs.Geninterp
Interpretation functions for generic arguments and interpreted Ltac values.Gensubst
GlobEnv
Type of environment extended with naming and ltac interpretation dataGlob_ops
Glob_term
Untyped intermediate termsHeads
This module is about the computation of an approximation of the head symbol of defined constants and local definitions; it provides the function to compute the head symbols and a table to store the headsIndrec
Errors related to recursors buildingInductiveops
The following three functions are similar to the ones defined in Inductive, but they expect an envKeys
Locus
Locus : positions in hypotheses and goalsLocusops
Utilities on or_varLtac_pretype
Nativenorm
This module implements normalization by evaluation to OCaml codePattern
Patternops
Pretype_errors
Pretyping
This file implements type inference. It maps glob_constr
(i.e. untyped terms whose names are located) to constr
. In particular, it drives complex pattern-matching problems ("match") into elementary ones, insertion of coercions and resolution of implicit arguments.Program
A bunch of Coq constants used by ProgramReductionops
Reduction Functions.Retyping
This family of functions assumes its constr argument is known to be well-typable. It does not type-check, just recompute the type without any costly verifications. On non well-typable terms, it either produces a wrong result or raise an anomaly. Use with care. It doesn't handle predicative universes too.Structures
Tacred
Typeclasses
Typeclasses_errors
Typing
This module provides the typing machine with existential variables and universes.Unification
Vnorm
This library exposes the following toplevel modules:
Genprint
Entry point for generic printersPpconstr
This module implements pretty-printers for constr_expr syntactic objects and their subcomponents.Ppextend
Pputils
Printer
These are the entry points for printing terms, context, tac, ...Proof_diffs
This library exposes the following toplevel modules:
Clenv
This file defines clausenv, which is a deprecated way to handle open terms in the proof engine. This API is legacy.Goal_select
Logic
Legacy proof engine. Do not use in newly written code.Miscprint
Printing of intro_pattern
Proof
Proof_bullet
Refine
The primitive refine tactic used to fill the holes in partial proofs. This is the recommended way to write tactics when the proof term is easy to write down. Note that this is not the user-level refine tactic defined in Ltac which is actually based on the one below.Tacmach
Operations for handling terms under a local typing context.Tactypes
Tactic-related types that are not totally Ltac specific and still used in lower API. It's not clear whether this is a temporary API or if this is meant to stay.This library exposes the following toplevel modules:
AsyncTaskQueue
Dag
Partac
ProofBlockDelimiter
Spawned
Stm
state-transaction-machine interfaceStmargs
TQueue
Vcs
WorkerPool
This library exposes the following toplevel modules:
Coqinit
Main etry point to the sysinit component, all other modules are private.Coqloadpath
This library exposes the following toplevel modules:
Abstract
Auto
This files implements auto and related automation tacticsAutorewrite
This files implements the autorewrite tactic.Btermdn
Discrimination nets with bounded depth.Cbn
Class_tactics
This files implements typeclasses eautoContradiction
DeclareScheme
Dn
EClause
Eauto
Elim
Eliminations tactics.Elimschemes
Induction/recursion schemesEqdecide
Eqschemes
This file builds schemes relative to equality inductive typesEquality
Evar_tactics
Generalize
Genredexpr
Reduction expressionsHints
Hipattern
High-order patternsInd_tables
This module provides support for registering inductive scheme builders, declaring schemes and generating schemes on demandInduction
Inv
Ppred
Redexpr
Interpretation layer of redexprs such as hnf, cbv, etc.Redops
Rewrite
TODO: document and clean me!Stdarg
Basic generic arguments.Tacticals
Tactics
Main tactics defined in ML. This file is huge and should probably be split in more reasonable units at some point. Because of its size and age, the implementation features various styles and stages of the proof engine. This has to be uniformized someday.This library exposes the following toplevel modules:
Ccompile
Colors
Initializer color for outputCommon_compile
Coqc
Coqcargs
Coqloop
The Coq toplevel loop.Coqrc
Coqtop
Definition of custom toplevels. init_extra
is used to do custom initialization run
launches a custom toplevel.G_toplevel
Load
Memtrace_init
Vernac
WorkerLoop
This library exposes the following toplevel modules:
Assumptions
Attributes
Auto_ind_decl
This file is about the automatic generation of schemes about decidable equality,Canonical
Classes
Instance declarationComArguments
ComAssumption
ComCoercion
Classes and coercions.ComDefinition
ComExtraDeps
ComFixpoint
ComHints
ComInductive
ComPrimitive
ComRewriteRule
ComSearch
ComTactic
DebugHook
Ltac debugger interface; clients should register hooks to interact with their provided interface.Declare
This module provides the functions to declare new variables, parameters, constants and inductive types in the global environment. It also updates some accessory tables such as Nametab
(name resolution), Impargs
, and Notations
.DeclareInd
Registering a mutual inductive definition together with its associated schemesDeclareUniv
Declaremods
Egramml
Mapping of grammar productions to camlp5 actions.Egramrocq
Mapping of grammar productions to camlp5 actionsFuture
G_proofs
G_redexpr
G_vernac
Himsg
This module provides functions to explain the type errors.Indschemes
Library
This module provides functions to load, open and save libraries. Libraries correspond to the subclass of modules that coincide with a file on disk (the ".vo" files). Libraries on the disk comes with checksums (obtained with the Digest
module), which are checked at loading time to prevent inconsistencies between files written at various dates.Loadpath
* Load paths.Metasyntax
Mltop
Opaques
Ppvernac
This module implements pretty-printers for vernac_expr syntactic objects and their subcomponents.Prettyp
This module implements Print/About/Locate commandsPrintmod
Proof_using
Utility code for section variables handling in Proof using...Pvernac
RecLemmas
Record
RetrieveObl
Search
Synterp
This module implements the syntactic interpretation phase of vernacular commands. The main entry point is synterp_control
, which transforms a vernacexpr into a vernac_control_entry
.Topfmt
Console printing optionsVernacControl
Vernac_classifier
Vernacentries
Vernacexpr
Vernacextend
Vernacular Extension dataVernacinterp
Vernacoptions
Vernacprop
Vernacstate
Vernactypes
Interpretation of extended vernac phrases.The entry point of this library is the module: Coqrun
.