Contents Menu Expand Light mode Dark mode Auto light/dark, in light mode Auto light/dark, in dark mode Skip to content
Dune documentation
Dune documentation
  • Getting Started and Core Concepts
    • Overview
    • Quickstart
    • Command-Line Interface
  • Tutorials
    • Developing with Dune
      • Introduction
      • Improving Structure
      • The Development Cycle
      • Interfacing with C
      • Using a PPX Preprocessor
      • Unit Tests
      • Conclusion
    • OCaml Package Management With Dune
      • Setting Up Package Management With Dune
      • Managing Dependencies
      • Pinning Projects
      • Custom Repositories
      • Locking Your Dependencies
      • Setting up an OxCaml project
  • How-to Guides
    • How to Install Dune
    • How to Set up Automatic Formatting
    • How to Generate Opam Files from dune-project
    • Cross-Compilation
    • Dealing with Foreign Libraries
    • Generating Documentation
    • How to Load Additional Files at Runtime
    • Instrumentation
    • JavaScript Compilation With Js_of_ocaml
    • Wasm Compilation With Wasm_of_ocaml
    • JavaScript Compilation With Melange
    • Virtual Libraries
    • Writing and Running Tests
    • How to Bundle Resources
    • How to Load a Project in a Toplevel
    • Using Rule Generation
    • How to Override the Default C Entrypoint With C Stubs
    • How to Release a Binary Distribution of an Application on Github with Dune
    • How to make a Homebrew Package with Dune
    • How to Use Opam Alongside Dune Package Management
    • How to Configure Editors with Package Management
    • How to Customize Lock Directories of Developer Tools
  • Reference Manual
    • dune
      • executable
      • executables
      • library
      • foreign_library
      • deprecated_library_name
      • generate_sites_module
      • test
      • tests
      • Cram
      • toplevel
      • documentation
      • install
      • plugin
      • rule
      • alias
      • copy_files
      • include
      • dynamic_include
      • env
      • dirs
      • files
      • data_only_dirs
      • ignored_subdirs
      • include_subdirs
      • vendored_dirs
      • subdir
      • cinaps
      • rocq.theory
      • coq.theory
      • mdx
      • menhir
      • ocamllex
      • ocamlyacc
      • library_parameter
      • jbuild_version
    • dune-project
      • accept_alternative_dune_file_name
      • authors
      • bug_reports
      • cram
      • dialect
      • Default dialects
      • documentation
      • executables_implicit_empty_intf
      • expand_aliases_in_sandbox
      • explicit_js_mode
      • formatting
      • generate_opam_files
      • homepage
      • implicit_transitive_deps
      • license
      • maintainers
      • maintenance_intent
      • map_workspace_root
      • name
      • opam_file_location
      • package
      • pin
      • source
      • subst
      • use_standard_c_and_cxx_flags
      • using
      • version
      • warnings
      • wrapped_executables
    • dune-workspace
      • config stanzas
      • context
      • env
      • lock_dir
      • pin
      • profile
      • repository
    • config
      • action_stdout_on_success
      • action_stderr_on_success
      • cache
      • cache-check-probability
      • cache-storage-mode
      • display
      • jobs
      • pkg
      • project_defaults
      • sandboxing_preference
      • terminal-persistence
    • Lexical Conventions
    • Actions
      • run
      • system
      • bash
      • dynamic-run
      • chdir
      • setenv
      • with-accepted-exit-codes
      • echo
      • with-<outputs>-to
      • with-stdin-from
      • ignore-<outputs>
      • cat
      • copy
      • copy#
      • write-file
      • pipe-<outputs>
      • cat
      • diff
      • diff?
      • cmp
      • progn
      • concurrent
      • no-infer
    • Ordered Set Language
    • Boolean Language
    • Predicate Language
    • Library Dependencies
    • Preprocessing Specification
    • Cram Tests
    • Variables
    • Dependency Specification
    • OCaml Flags
    • Sandboxing
    • Locks
    • Diffing and Promotion
    • Diffing
    • Promotion
    • Package Specification
    • Aliases
      • @all
      • @default
      • @install
      • @pkg-install
      • @empty
      • @check
      • @ocaml-index
      • @runtest
      • @fmt
      • @lint
      • @unused-libs
      • @doc
      • @doc-private
      • @doc-json
    • Foreign Stubs
    • Foreign Archives
    • Extra Objects
    • Flags in Foreign Code
    • Command Line Interface
    • Dune Libraries
    • Dune Caches
    • How Caching Works
    • Configuration
    • Cache Storage Mode
    • Trimming the Cache
    • Reproducibility
    • The Rocq Prover Build Language
    • Coq
    • Dune RPC
    • Packages
    • Findlib Integration
  • Explanation
    • The Dune Mental Model
    • Dune Projects and Workspaces
    • How Preprocessing Works
    • The OCaml Ecosystem
    • How Package Management Works
    • How Dune integrates with opam
    • How Dune Uses Dune to Build Dune
    • A Tour of the Dune Codebase
      • Command-Line Interface
      • Parsing of Dune Files
      • Rule Generation
      • The Engine
      • Libraries
      • Vendored Libraries
      • Tests
  • Advanced Topics
    • Dynamic Loading of Packages with Findlib
    • Profiling Dune
    • Package Version
    • OCaml Syntax
    • Variables for Artifacts
    • Building an Ad Hoc .cmxs
  • Miscellaneous
    • FAQ
    • Goal of Dune
    • Working on the Dune Codebase
Back to top
Edit this page
View this page

rocq.theory¶

See the documentation on the rocq.theory, rocq.extraction, rocq.pp, and related stanzas.

Next
coq.theory
Previous
cinaps
Copyright © 2017 - 2025, Jérémie Dimino & the Dune maintainers
Made with Sphinx and @pradyunsg's Furo