package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/src/rocq-runtime.config/coq_config.ml.html
Source file coq_config.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73
(* DO NOT EDIT THIS FILE: automatically generated by ../configure *) (* Exact command that generated this file: *) (* _build/default/tools/configure/configure.exe -prefix /home/opam/.opam/5.3 -mandir /home/opam/.opam/5.3/man -libdir /home/opam/.opam/5.3/lib/coq -native-compiler no *) let install_prefix = "/home/opam/.opam/5.3" let coqlib = "/home/opam/.opam/5.3/lib/coq" let configdir = "/home/opam/.opam/5.3/etc/xdg/coq" let datadir = "/home/opam/.opam/5.3/share/coq" let docdir = "/home/opam/.opam/5.3/share/doc" let coqlibsuffix = "lib/coq" let configdirsuffix = "etc/xdg/coq" let datadirsuffix = "share/coq" let docdirsuffix = "share/doc" let ocamlfind = "/home/opam/.opam/5.3/bin/ocamlfind" let caml_flags = "-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70" let version = "9.0.0" let caml_version = "5.3.0" let caml_version_nums = [5;3;0] let arch = "Linux" let arch_is_win32 = false let exec_extension = "" let has_natdynlink = true let vo_version = 90000l let browser = "xdg-open \"%s\"" let wwwcoq = "http://coq.inria.fr/" let wwwbugtracker = "http://coq.inria.fr/bugs/" let wwwrefman = "http://coq.inria.fr/doc/V9.0.0/refman/" let wwwstdlib = "http://coq.inria.fr/doc/V9.0.0/stdlib/" let bytecode_compiler = true type native_compiler = NativeOff | NativeOn of { ondemand : bool } let native_compiler = NativeOff let core_src_dirs = [ "boot"; "config"; "lib"; "clib"; "kernel"; "library"; "engine"; "pretyping"; "interp"; "gramlib"; "parsing"; "proofs"; "tactics"; "toplevel"; "printing"; "ide"; "stm"; "vernac"; ] let plugins_dirs = [ "plugins/btauto"; "plugins/cc"; "plugins/derive"; "plugins/extraction"; "plugins/firstorder"; "plugins/funind"; "plugins/ltac"; "plugins/ltac2"; "plugins/ltac2_ltac1"; "plugins/micromega"; "plugins/nsatz"; "plugins/ring"; "plugins/rtauto"; "plugins/ssr"; "plugins/ssrmatching"; "plugins/syntax"; ] let all_src_dirs = core_src_dirs @ plugins_dirs
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>