package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.19.2.tar.gz
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c
doc/src/coq-core.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
(* 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 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 = "8.19.2" 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 = 81999l let browser = "firefox -remote \"OpenURL(%s,new-tab)\" || firefox %s &" let wwwcoq = "http://coq.inria.fr/" let wwwbugtracker = "http://coq.inria.fr/bugs/" let wwwrefman = "http://coq.inria.fr/doc/V8.19.2/refman/" let wwwstdlib = "http://coq.inria.fr/doc/V8.19.2/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/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)"
>