From 598e3ae4a8eb8d9bce316e13d71ee48d9ba1a01f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 28 Oct 2017 21:02:48 +0200 Subject: [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. --- lib/flags.ml | 8 -------- 1 file changed, 8 deletions(-) (limited to 'lib/flags.ml') diff --git a/lib/flags.ml b/lib/flags.ml index ddc8f8482..97795faa6 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -179,14 +179,6 @@ let is_standard_doc_url url = let coqlib_spec = ref false let coqlib = ref "(not initialized yet)" -(* Options for changing ocamlfind (used by coqmktop) *) -let ocamlfind_spec = ref false -let ocamlfind = ref Coq_config.camlbin - -(* Options for changing camlp4bin (used by coqmktop) *) -let camlp4bin_spec = ref false -let camlp4bin = ref Coq_config.camlp4bin - (* Level of inlining during a functor application *) let default_inline_level = 100 -- cgit v1.2.3