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-FindTop_printers Printers for the OCaml toplevel.Vm_printers 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 Rocq 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 Abbreviation Abbreviations.Constrexpr Constrexpr_ops Constrexpr_ops: utilities on constr_exprConstrextern 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_constrNotationextern 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 referenceCClosure Lazy reduction.CPrimitives Constant_typing Constr This file defines the most important datatype of Rocq, 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 ValuesAcyclicGraph Graphs representing strict ordersAux_file CAst CDebug CErrors This modules implements basic manipulations of errors for use throughout Rocq's code.CWarnings Control Global control of Rocq.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 Rocq 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 Rocq 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 Rocq 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 Rocq 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 Coqlib Deprecated alias for RocqlibGlobal This module defines the global environment of Rocq. 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 CLexer Extend Entry keys for constr notationsG_constr G_prim Notation_gram Notgram_ops Pcoq Deprecated alias for ProcqProcq The parser of RocqTok The type of token for the Rocq lexer and parserPerf Global CPU instruction counter.No module.
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 Rocq 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 Rocq 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 TemplateArity Typeclasses Typeclasses_errors Typing This module provides the typing machine with existential variables and universes.Unification Vnorm 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 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_patternProof 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.AsyncTaskQueue Dag Partac ProofBlockDelimiter Spawned Stm state-transaction-machine interfaceStmargs TQueue Vcs WorkerPool Coqinit Main etry point to the sysinit component, all other modules are private.Coqloadpath 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.Ccompile Colors Initializer color for outputCommon_compile Coqc Coqcargs Coqloop The Rocq 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 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.