aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/flags.mli
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-14 00:06:02 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-14 00:06:02 +0100
commit290abf59e6f13bb1468d8e3df050cf0bd9c48708 (patch)
treea61d3dce0bd34372b48668f44d280b5d886e2994 /lib/flags.mli
parent7576ffd4eb196d5d5a15f6cacb2ba5cba00576ef (diff)
parentf5cb7eb3e68e4b7d1bb5eeb8d9c58666201945d4 (diff)
Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.
Diffstat (limited to 'lib/flags.mli')
-rw-r--r--lib/flags.mli6
1 files changed, 0 insertions, 6 deletions
diff --git a/lib/flags.mli b/lib/flags.mli
index b82fe6128..1b1e264f0 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -122,12 +122,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