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.mli | 6 ------ 1 file changed, 6 deletions(-) (limited to 'lib/flags.mli') diff --git a/lib/flags.mli b/lib/flags.mli index c4afb8318..e4710a126 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -143,12 +143,6 @@ val is_standard_doc_url : string -> bool val coqlib_spec : bool ref val coqlib : string ref -(** Options for specifying where OCaml binaries reside *) -val ocamlfind_spec : bool ref -val ocamlfind : string ref -val camlp4bin_spec : bool ref -val camlp4bin : string ref - (** Level of inlining during a functor application *) val set_inline_level : int -> unit val get_inline_level : unit -> int -- cgit v1.2.3