package rocq-runtime

  1. Overview
  2. Docs
On This Page
  1. API
    1. Library btauto_plugin
    2. Library byte_config
    3. Library cc_core_plugin
    4. Library cc_plugin
    5. Library derive_plugin
    6. Library extraction_plugin
    7. Library firstorder_core_plugin
    8. Library firstorder_plugin
    9. Library funind_plugin
    10. Library ltac2_ltac1_plugin
    11. Library ltac2_plugin
    12. Library ltac_plugin
    13. Library micromega_core_plugin
    14. Library micromega_plugin
    15. Library nsatz_core_plugin
    16. Library nsatz_plugin
    17. Library number_string_notation_plugin
    18. Library ring_plugin
    19. Library rocq-runtime.boot
    20. Library rocq-runtime.checklib
    21. Library rocq-runtime.clib
    22. Library rocq-runtime.config
    23. Library rocq-runtime.coqargs
    24. Library rocq-runtime.coqdeplib
    25. Library rocq-runtime.coqworkmgrapi
    26. Library rocq-runtime.debugger_support
    27. Library rocq-runtime.dev
    28. Library rocq-runtime.engine
    29. Library rocq-runtime.gramlib
    30. Library rocq-runtime.interp
    31. Library rocq-runtime.kernel
    32. Library rocq-runtime.lib
    33. Library rocq-runtime.library
    34. Library rocq-runtime.parsing
    35. Library rocq-runtime.perf
    36. Library rocq-runtime.pretyping
    37. Library rocq-runtime.printing
    38. Library rocq-runtime.proofs
    39. Library rocq-runtime.rocqshim
    40. Library rocq-runtime.stm
    41. Library rocq-runtime.sysinit
    42. Library rocq-runtime.tactics
    43. Library rocq-runtime.toplevel
    44. Library rocq-runtime.vernac
    45. Library rocq-runtime.vm
    46. Library rtauto_plugin
    47. Library ssreflect_plugin
    48. Library ssrmatching_plugin
    49. Library tauto_plugin
    50. Library tuto0_plugin
    51. Library tuto1_plugin
    52. Library tuto2_plugin
    53. Library tuto3_plugin
    54. Library zify_plugin
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

rocq-runtime

API

Library btauto_plugin

Library byte_config

Library cc_core_plugin

Library cc_plugin

Library derive_plugin

Library extraction_plugin

Library firstorder_core_plugin

Library firstorder_plugin

Library funind_plugin

Library ltac2_ltac1_plugin

Library ltac2_plugin

Library ltac_plugin

Library micromega_core_plugin

Library micromega_plugin

Library nsatz_core_plugin

Library nsatz_plugin

Library number_string_notation_plugin

Library ring_plugin

Library rocq-runtime.boot

Library rocq-runtime.checklib

Library rocq-runtime.clib

Library rocq-runtime.config

Library rocq-runtime.coqargs

Library rocq-runtime.coqdeplib

Library rocq-runtime.coqworkmgrapi

Library rocq-runtime.debugger_support

Library rocq-runtime.dev

Library rocq-runtime.engine

  • 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 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 names
  • Profile_tactic Ltac profiling primitives
  • 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.
  • UnivFlex
  • UnivGen
  • UnivMinim
  • UnivNames Local universe name <-> level mapping
  • UnivProblem
  • UnivSubst

Library rocq-runtime.gramlib

Library rocq-runtime.interp

  • 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 Constr default entries
  • 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

Library rocq-runtime.kernel

  • CClosure 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 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.
  • HConstr
  • 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
  • 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 reduction
  • 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
  • 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 Values

Library rocq-runtime.lib

  • AcyclicGraph Graphs representing strict orders
  • Aux_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

Library rocq-runtime.library

  • Coqlib Deprecated alias for Rocqlib
  • 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
  • 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:
  • Library_info
  • Locality * Managing locality
  • Nametab This module contains the tables for globalization.
  • Rocqlib Indirection between logical names and global references.
  • Summary

Library rocq-runtime.parsing

Library rocq-runtime.perf

  • Perf Global CPU instruction counter.

Library rocq-runtime.pretyping

  • 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 terms
  • Detyping
  • 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 occurrences
  • Genarg 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 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 Rocq 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
  • TemplateArity
  • Typeclasses
  • Typeclasses_errors
  • Typing This module provides the typing machine with existential variables and universes.
  • Unification
  • Vnorm

Library rocq-runtime.printing

  • 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

Library rocq-runtime.proofs

  • 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.

Library rocq-runtime.rocqshim

Library rocq-runtime.stm

Library rocq-runtime.sysinit

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

Library rocq-runtime.tactics

Library rocq-runtime.toplevel

Library rocq-runtime.vernac

Library rocq-runtime.vm

Library rtauto_plugin

Library ssreflect_plugin

Library ssrmatching_plugin

Library tauto_plugin

Library tuto0_plugin

Library tuto1_plugin

Library tuto2_plugin

Library tuto3_plugin

Library zify_plugin

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