aboutsummaryrefslogtreecommitdiffhomepage
path: root/config
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-10-28 21:02:48 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-10 18:41:16 +0100
commit598e3ae4a8eb8d9bce316e13d71ee48d9ba1a01f (patch)
tree7bf3135dea14dfccac59a6b373549b6bddec7741 /config
parentd0f89f8c59cda2e7e74fec693e511e910fbc0434 (diff)
[build] Remove coqmktop in favor of ocamlfind.
We remove coqmktop in favor of a couple of simple makefile rules using ocamlfind. In order to do that, we introduce a new top-level file that calls the coqtop main entry. This is very convenient in order to use other builds systems such as `ocamlbuild` or `jbuilder`. An additional consideration is that we must perform a side-effect on init depending on whether we have an OCaml toplevel available [byte] or not. We do that by using two different object files, one for the bytecode version other for the native one, but we may want to review our choice. We also perform some smaller cleanups taking profit from ocamlfind.
Diffstat (limited to 'config')
-rw-r--r--config/coq_config.mli4
1 files changed, 0 insertions, 4 deletions
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 6a834a304..40661f428 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -41,12 +41,8 @@ val caml_flags : string (* arguments passed to ocamlc (ie. CAMLFLAGS) *)
val best : string (* byte/opt *)
val arch : string (* architecture *)
val arch_is_win32 : bool
-val osdeplibs : string (* OS dependent link options for ocamlc *)
val vmbyteflags : string list (* -custom/-dllib -lcoqrun *)
-
-(* val defined : string list (* options for lib/ocamlpp *) *)
-
val version : string (* version number of Coq *)
val caml_version : string (* OCaml version used to compile Coq *)
val caml_version_nums : int list (* OCaml version used to compile Coq by components *)