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
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 = "8.20.1"
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 = 82000l
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.20.1/refman/"
let wwwstdlib = "http://coq.inria.fr/doc/V8.20.1/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