package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (6)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.3.0.tar.gz
sha256=3f0fc283e8644394aa9c7a6e3995b6d9ebbe1e6dda712bf431f9c372dcef95ad

doc/rocq-runtime.config/Coq_config/index.html

Module Coq_configSource

Sourceval gc_ramp_up : (unit -> 'a) -> 'a

If available (OCaml >=5.4), Gc.ramp_up dropping the suspended_collection_work data. Otherwise just call the given function.

Sourcetype relocatable_path =
  1. | NotRelocatable of string
  2. | Relocatable of string
Sourceval install_prefix : relocatable_path
Sourceval configdir : relocatable_path
Sourceval coqlibsuffix : string
Sourceval configdirsuffix : string
Sourceval datadirsuffix : string
Sourceval docdirsuffix : string
Sourceval ocamlfind : string
Sourceval caml_flags : string
Sourceval arch : string
Sourceval arch_is_win32 : bool
Sourceval version : string
Sourceval caml_version : string
Sourceval caml_version_nums : int list
Sourceval vo_version : int32
Sourceval all_src_dirs : string list
Sourceval exec_extension : string
Sourceval browser : string

default web browser to use, may be overridden by environment variable COQREMOTEBROWSER

Sourceval wwwcoq : string
Sourceval wwwcorelib : string
Sourceval wwwrefman : string
Sourceval wwwbugtracker : string
Sourceval bytecode_compiler : bool
Sourcetype native_compiler =
  1. | NativeOff
  2. | NativeOn of {
    1. ondemand : bool;
    }
Sourceval native_compiler : native_compiler