package rocq-runtime

  1. Overview
  2. Docs
On This Page
  1. Libraries
    1. rocq-runtime.boot
    2. rocq-runtime.checklib
    3. rocq-runtime.clib
    4. rocq-runtime.config
    5. rocq-runtime.config.byte
    6. rocq-runtime.coqargs
    7. rocq-runtime.coqdeplib
    8. rocq-runtime.coqworkmgrapi
    9. rocq-runtime.debugger_support
    10. rocq-runtime.dev
    11. rocq-runtime.engine
    12. rocq-runtime.gramlib
    13. rocq-runtime.interp
    14. rocq-runtime.kernel
    15. rocq-runtime.lib
    16. rocq-runtime.library
    17. rocq-runtime.parsing
    18. rocq-runtime.perf
    19. rocq-runtime.plugins.btauto
    20. rocq-runtime.plugins.cc
    21. rocq-runtime.plugins.cc_core
    22. rocq-runtime.plugins.derive
    23. rocq-runtime.plugins.extraction
    24. rocq-runtime.plugins.firstorder
    25. rocq-runtime.plugins.firstorder_core
    26. rocq-runtime.plugins.funind
    27. rocq-runtime.plugins.ltac
    28. rocq-runtime.plugins.ltac2
    29. rocq-runtime.plugins.ltac2_ltac1
    30. rocq-runtime.plugins.micromega
    31. rocq-runtime.plugins.micromega_core
    32. rocq-runtime.plugins.nsatz
    33. rocq-runtime.plugins.nsatz_core
    34. rocq-runtime.plugins.number_string_notation
    35. rocq-runtime.plugins.ring
    36. rocq-runtime.plugins.rtauto
    37. rocq-runtime.plugins.ssreflect
    38. rocq-runtime.plugins.ssrmatching
    39. rocq-runtime.plugins.tauto
    40. rocq-runtime.plugins.tutorial.p0
    41. rocq-runtime.plugins.tutorial.p1
    42. rocq-runtime.plugins.tutorial.p2
    43. rocq-runtime.plugins.tutorial.p3
    44. rocq-runtime.plugins.zify
    45. rocq-runtime.pretyping
    46. rocq-runtime.printing
    47. rocq-runtime.proofs
    48. rocq-runtime.rocqshim
    49. rocq-runtime.stm
    50. rocq-runtime.sysinit
    51. rocq-runtime.tactics
    52. rocq-runtime.toplevel
    53. rocq-runtime.vernac
    54. rocq-runtime.vm
package rocq-runtime
Legend:
Library
Module
Module type
Parameter
Class
Class type

rocq-runtime 9.0.0

Libraries

This package provides the following libraries (via ocamlobjinfo):

rocq-runtime.boot

Documentation:

rocq-runtime.checklib

Documentation:

rocq-runtime.clib

Documentation:

rocq-runtime.config

Documentation:

rocq-runtime.config.byte

Documentation:

rocq-runtime.coqargs

Documentation:

rocq-runtime.coqdeplib

Documentation:

rocq-runtime.coqworkmgrapi

Documentation:

rocq-runtime.debugger_support

Documentation:

rocq-runtime.dev

Documentation:

rocq-runtime.engine

Documentation:

  • UnivSubst
  • UnivProblem
  • UnivNames Local universe name <-> level mapping
  • UnivFlex
  • UnivMinim
  • UnivGen
  • 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.
  • Evar_kinds The kinds of existential variable
  • Nameops Identifiers and names
  • 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.
  • EConstr
  • Namegen This file features facilities to generate fresh names.
  • Termops This file defines various utilities for term manipulation that are not needed in the kernel.
  • 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.
  • 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.
  • Evarutil This module provides useful higher-level functions for evar manipulation.
  • 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.
  • Profile_tactic Ltac profiling primitives
  • 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.

rocq-runtime.gramlib

Documentation:

rocq-runtime.interp

Documentation:

  • NumTok Numbers in different forms: signed or unsigned, possibly with fractional part and exponent.
  • Notation_ops Constr default entries
  • Notationextern Declaration of uninterpretation functions (i.e. printing rules) for notations
  • Abbreviation Abbreviations.
  • Notation Notations
  • 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
  • Reserve
  • Constrexpr_ops Constrexpr_ops: utilities on constr_expr
  • 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
  • Constrintern Translation from front abstract syntax of term to untyped terms (glob_constr)
  • Modintern Module internalization errors
  • Constrextern Translation of pattern, cases pattern, glob_constr and term into syntax trees for printing

rocq-runtime.kernel

Documentation:

  • 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.
  • Uint63
  • Float64_common
  • Float64
  • 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:
  • Parray
  • Partial_subst
  • Pstring Primitive string type.
  • Univ
  • Sorts
  • UVars
  • Vmvalues Values
  • Context The modules defined below represent a local context as defined by Chapter 4 in the Reference Manual:
  • Esubst Explicit substitutions
  • UGraph
  • Constr This file defines the most important datatype of Rocq, namely kernel terms, as well as a handful of generic manipulation functions.
  • CPrimitives
  • TransparentState
  • Conv_oracle
  • Vars
  • Term
  • Cooking
  • Retroknowledge
  • Mod_subst
  • Opaqueproof This module implements the handling of opaque proof terms. Opaque proof terms are special since:
  • Rtree
  • Vmbytecodes
  • Vmerrors
  • Vmopcodes
  • Vmemitcodes
  • Vmlibrary
  • Declareops Operations concerning types in Declarations : constant_body, mutual_inductive_body, module_body ...
  • 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.
  • Primred
  • 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 reduction
  • CClosure Lazy reduction.
  • Reduction None of these functions do eta reduction
  • Type_errors Type errors. \label{typeerrors}
  • Inductive
  • Genlambda Intermediate language used by both the VM and native.
  • Vmlambda
  • Vmbytegen
  • Vmsymtable
  • Vm
  • Conversion
  • Vconv
  • HConstr
  • 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.
  • Nativelambda This file defines the lambda code generation phase of the native compiler
  • 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.
  • Nativelib This file provides facilities to access OCaml compiler and dynamic linker, used by the native compiler.
  • Nativeconv This module implements the conversion test by compiling to OCaml code
  • Typeops
  • Modops
  • Subtyping
  • Section Kernel implementation of sections.
  • 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.
  • Constant_typing
  • Discharge
  • InferCumulativity
  • IndTyping
  • Indtypes
  • Mod_typing Main functions for translating module entries
  • Nativelibrary This file implements separate compilation for libraries in the native compiler
  • Safe_typing

rocq-runtime.lib

Documentation:

  • Util This module contains numerous utility functions on strings, lists, arrays, etc.
  • Control Global control of Rocq.
  • Flags Global options of the system.
  • Pp Rocq document type.
  • Loc
  • Quickfix
  • CErrors This modules implements basic manipulations of errors for use throughout Rocq's code.
  • Stateid
  • Feedback
  • CWarnings
  • Deprecation
  • UserWarn This is about warnings triggered from user .v code ("warn" attibute). See cWarnings.mli for the generic warning interface.
  • Instr Platform-specific Implementation of a global instruction counter.
  • System
  • CDebug
  • Spawn
  • 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.
  • ObjFile
  • 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).
  • NewProfile
  • Hook This module centralizes the notions of hooks. Hooks are pointers that are to be set at runtime exactly once.
  • CAst
  • DAst Lazy AST node wrapper. Only used for glob_constr as of today.
  • CoqProject_file
  • Aux_file
  • AcyclicGraph Graphs representing strict orders

rocq-runtime.library

Documentation:

  • Summary
  • Global 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
  • Libnames
  • Nametab This module contains the tables for globalization.
  • Libobject Libobject declares persistent objects, given with methods:
  • Library_info
  • Lib Lib: record of operations, backtrack, low-level sections
  • Rocqlib Indirection between logical names and global references.
  • Locality * Managing locality
  • Goptions This module manages customization parameters at the vernacular level
  • Coqlib Deprecated alias for Rocqlib

rocq-runtime.parsing

Documentation:

rocq-runtime.perf

Documentation:

  • Perf Global CPU instruction counter.

rocq-runtime.plugins.btauto

Documentation:

rocq-runtime.plugins.cc

Documentation:

rocq-runtime.plugins.cc_core

Documentation:

rocq-runtime.plugins.derive

Documentation:

rocq-runtime.plugins.extraction

Documentation:

rocq-runtime.plugins.firstorder

Documentation:

rocq-runtime.plugins.firstorder_core

Documentation:

rocq-runtime.plugins.funind

Documentation:

rocq-runtime.plugins.ltac

Documentation:

rocq-runtime.plugins.ltac2

Documentation:

rocq-runtime.plugins.ltac2_ltac1

Documentation:

rocq-runtime.plugins.micromega

Documentation:

rocq-runtime.plugins.micromega_core

Documentation:

rocq-runtime.plugins.nsatz

Documentation:

rocq-runtime.plugins.nsatz_core

Documentation:

rocq-runtime.plugins.number_string_notation

Documentation:

rocq-runtime.plugins.ring

Documentation:

rocq-runtime.plugins.rtauto

Documentation:

rocq-runtime.plugins.ssreflect

Documentation:

rocq-runtime.plugins.ssrmatching

Documentation:

rocq-runtime.plugins.tauto

Documentation:

rocq-runtime.plugins.tutorial.p0

Documentation:

rocq-runtime.plugins.tutorial.p1

Documentation:

rocq-runtime.plugins.tutorial.p2

Documentation:

rocq-runtime.plugins.tutorial.p3

Documentation:

rocq-runtime.plugins.zify

Documentation:

rocq-runtime.pretyping

Documentation:

  • Evaluable Evaluable references (whose transparency can be controlled)
  • Arguments_renaming
  • Reductionops Reduction Functions.
  • Pretype_errors
  • Inductiveops The following three functions are similar to the ones defined in Inductive, but they expect an env
  • TemplateArity
  • 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.
  • Vnorm
  • Genarg Generic arguments used by the extension mechanisms of several Rocq ASTs.
  • Geninterp Interpretation functions for generic arguments and interpreted Ltac values.
  • Cbv
  • Glob_ops
  • Gensubst
  • Structures
  • Patternops
  • Constr_matching This module implements pattern-matching on terms
  • Evarsolve
  • Locusops Utilities on or_var
  • Find_subterm Finding subterms, possibly up to some unification function, possibly at some given occurrences
  • Evardefine
  • Evarconv
  • Typing This module provides the typing machine with existential variables and universes.
  • Tacred
  • Coercionops
  • 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
  • Program A bunch of Rocq constants used by Program
  • Typeclasses_errors
  • Typeclasses
  • Coercion
  • Keys
  • Unification
  • GlobEnv Type of environment extended with naming and ltac interpretation data
  • Cases
  • 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.
  • Nativenorm This module implements normalization by evaluation to OCaml code
  • Indrec Errors related to recursors building
  • Detyping
  • 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:

rocq-runtime.printing

Documentation:

  • Ppextend
  • Genprint Entry point for generic printers
  • Pputils
  • Ppconstr This module implements pretty-printers for constr_expr syntactic objects and their subcomponents.
  • Proof_diffs
  • Printer These are the entry points for printing terms, context, tac, ...

rocq-runtime.proofs

Documentation:

  • Logic Legacy proof engine. Do not use in newly written code.
  • Tacmach Operations for handling terms under a local typing context.
  • 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.
  • Goal_select
  • Proof
  • Proof_bullet
  • Miscprint Printing of intro_pattern
  • Clenv This file defines clausenv, which is a deprecated way to handle open terms in the proof engine. This API is legacy.

rocq-runtime.rocqshim

Documentation:

rocq-runtime.stm

Documentation:

rocq-runtime.sysinit

Documentation:

  • Coqloadpath
  • Coqinit Main etry point to the sysinit component, all other modules are private.

rocq-runtime.tactics

Documentation:

rocq-runtime.toplevel

Documentation:

rocq-runtime.vernac

Documentation:

rocq-runtime.vm

Documentation:

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct