The entry point of this library is the module: `Boot`

.

This library exposes the following toplevel modules:

`CArray`

`CEphemeron`

`CList`

`CMap`

`CObj`

`CSet`

`CSig`

Missing pervasive types from OCaml stdlib`CString`

`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 values`Exninfo`

Additional information worn by exceptions.`HMap`

`Hashcons`

Generic hash-consing.`Hashset`

Adapted from Damien Doligez, projet Para, INRIA Rocquencourt, OCaml stdlib.`Heap`

Heaps`IStream`

`Int`

A native integer module with usual utility functions.`Monad`

Combinators on monadic computations.`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 lists`SList`

Sparse lists.`Segmenttree`

This module is a very simple implementation of "segment trees".`Store`

`Terminal`

`Trie`

Generic functorized trie data structure.`Unicode`

Unicode utilities`Unicodetable`

`Unionfind`

An imperative implementation of partitions via Union-Find

The entry point of this library is the module: `Coq_config`

.

The entry point of this library is the module: `CoqworkmgrApi`

.

This library exposes the following toplevel modules:

`EConstr`

`Evar_kinds`

The kinds of existential variable`Evarutil`

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 names`Proofview`

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.`UnivGen`

`UnivMinim`

`UnivNames`

Local universe name <-> level mapping`UnivProblem`

`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 printing`Constrintern`

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 errors`Notation`

Notations`Notation_ops`

`Notation_term`

`notation_constr`

`Notationextern`

Declaration of uninterpretation functions (i.e. printing rules) for notations`NumTok`

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 reference`Stdarg`

Basic generic arguments.

This library exposes the following toplevel modules:

`CClosure`

`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 types`Declareops`

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 types`Environ`

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 substitutions`Evar`

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.`IndTyping`

`Indtypes`

`Inductive`

`InferCumulativity`

`Mod_subst`

`Mod_typing`

Main functions for translating module entries`Modops`

`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 code`Nativelambda`

This file defines the lambda code generation phase of the native compiler`Nativelib`

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 compiler`Nativevalues`

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`

`Primred`

`Reduction`

None of these functions do eta reduction`Relevanceops`

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`

`Safe_typing`

`Section`

Kernel implementation of sections.`Sorts`

`Subtyping`

`Term`

`TransparentState`

`Type_errors`

Type errors.`\label{typeerrors}`

`Typeops`

`UGraph`

`Uint63`

`Univ`

`Values`

`Vars`

`Vconv`

`Vm`

`Vmbytecodes`

`Vmbytegen`

`Vmemitcodes`

`Vmlambda`

`Vmopcodes`

`Vmsymtable`

`Vmvalues`

Values

This library exposes the following toplevel modules:

`AcyclicGraph`

Graphs representing strict orders`Aux_file`

`CAst`

`CDebug`

`CErrors`

This modules implements basic manipulations of errors for use throughout Coq's code.`CProfile`

`CWarnings`

`Control`

Global control of Coq.`CoqProject_file`

`Core_plugins_findlib_compat`

`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.`Loc`

`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.`Rtree`

`Spawn`

`Stateid`

`System`

`Util`

`Xml_datatype`

This library exposes the following toplevel modules:

`Coqlib`

Indirection between logical names and global references.`Global`

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 level`Lib`

Lib: record of operations, backtrack, low-level sections`Libnames`

`Libobject`

`Libobject`

declares persistent objects, given with methods:`Nametab`

This module contains the tables for globalization.`Summary`

This library exposes the following toplevel modules:

`CLexer`

`Extend`

Entry keys for constr notations`G_constr`

`G_prim`

`Notation_gram`

`Notgram_ops`

`Pcoq`

The parser of Coq`Tok`

The type of token for the Coq lexer and parser

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: `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: `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: `Micromega_plugin`

.

The entry point of this library is the module: `Nsatz_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`

`Constr_matching`

This module implements pattern-matching on terms`Detyping`

`Evarconv`

`Evardefine`

`Evarsolve`

`Find_subterm`

Finding subterms, possibly up to some unification function, possibly at some given occurrences`Genarg`

Generic arguments used by the extension mechanisms of several Coq ASTs.`Geninterp`

Interpretation functions for generic arguments and interpreted Ltac values.`GlobEnv`

Type of environment extended with naming and ltac interpretation data`Glob_ops`

`Glob_term`

Untyped intermediate terms`Heads`

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 heads`Indrec`

Errors related to recursors building`Inductiveops`

The following three functions are similar to the ones defined in Inductive, but they expect an env`Keys`

`Locus`

Locus : positions in hypotheses and goals`Locusops`

Utilities on or_var`Ltac_pretype`

`Nativenorm`

This module implements normalization by evaluation to OCaml code`Pattern`

`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 Program`Reductionops`

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 printers`Ppconstr`

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 interface`Stmargs`

`TQueue`

`Vcs`

`Vio_checking`

`WorkerPool`

This library exposes the following toplevel modules:

`Coqargs`

`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 tactics`Autorewrite`

This files implements the autorewrite tactic.`Btermdn`

Discrimination nets with bounded depth.`Cbn`

`Class_tactics`

This files implements typeclasses eauto`Contradiction`

`DeclareScheme`

`Dn`

`EClause`

`Eauto`

`Elim`

Eliminations tactics.`Elimschemes`

Induction/recursion schemes`Eqdecide`

`Eqschemes`

This file builds schemes relative to equality inductive types`Equality`

`Evar_tactics`

`Genredexpr`

Reduction expressions`Hints`

`Hipattern`

High-order patterns`Ind_tables`

This module provides support for registering inductive scheme builders, declaring schemes and generating schemes on demand`Inv`

`Ppred`

`Redexpr`

Interpretation layer of redexprs such as hnf, cbv, etc.`Redops`

`Rewrite`

TODO: document and clean me!`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.

The entry point of this library is the module: `Top_printers`

.

This library exposes the following toplevel modules:

`Ccompile`

`Colors`

Initializer color for output`Common_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`

`Vio_compile`

`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 declaration`ComArguments`

`ComAssumption`

`ComCoercion`

Classes and coercions.`ComDefinition`

`ComExtraDeps`

`ComFixpoint`

`ComHints`

`ComInductive`

`ComPrimitive`

`ComProgramFixpoint`

`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 accesory tables such as`Nametab`

(name resolution),`Impargs`

, and`Notations`

.`DeclareInd`

Registering a mutual inductive definition together with its associated schemes`DeclareUctx`

`DeclareUniv`

`Declaremods`

`Egramcoq`

Mapping of grammar productions to camlp5 actions`Egramml`

Mapping of grammar productions to camlp5 actions.`Future`

`G_proofs`

`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.`Locality`

* Managing locality`Metasyntax`

`Mltop`

`Opaques`

`Ppvernac`

This module implements pretty-printers for vernac_expr syntactic objects and their subcomponents.`Prettyp`

A Pretty-Printer for the Calculus of Inductive Constructions.`Printmod`

`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 options`Vernac_classifier`

`Vernacentries`

`Vernacexpr`

`Vernacextend`

Vernacular Extension data`Vernacinterp`

`Vernacoptions`

`Vernacprop`

`Vernacstate`

The entry point of this library is the module: `Coqrun`

.