aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--lib/envars.mli1
-rw-r--r--tools/coq_makefile.ml2
-rw-r--r--toplevel/usage.ml1
3 files changed, 1 insertions, 3 deletions
diff --git a/lib/envars.mli b/lib/envars.mli
index e99fd8e03..fbcbfe72a 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -26,6 +26,5 @@ val xdg_dirs : warn:(string -> unit) -> string list
val coqpath : string list
val camlbin : unit -> string
-val camlp4bin : unit -> string
val camllib : unit -> string
val camlp4lib : unit -> string
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index d7e34e059..4734fa6e7 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -380,7 +380,7 @@ CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo
else
CAMLP4EXTEND=
endif\n";
- print "PP?=-pp \"$(CAMLP4BIN)$(CAMLP4O) -I $(CAMLLIB) -I . $(COQSRCLIBS) compat5.cmo \\
+ print "PP?=-pp \"$(CAMLP4O) -I $(CAMLLIB) -I . $(COQSRCLIBS) compat5.cmo \\
$(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n\n";
end;
match is_install with
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index dcf11354b..9c0512464 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -100,7 +100,6 @@ let print_config () =
Printf.printf "CAMLLIB=%s/\n" (Envars.camllib ());
Printf.printf "CAMLP4=%s\n" Coq_config.camlp4;
Printf.printf "CAMLP4O=%s\n" Coq_config.camlp4o;
- Printf.printf "CAMLP4BIN=%s/\n" (Envars.camlp4bin ());
Printf.printf "CAMLP4LIB=%s\n" (Envars.camlp4lib ());
Printf.printf "CAMLP4OPTIONS=%s\n" Coq_config.camlp4compat;
Printf.printf "HASNATDYNLINK=%s\n" (if Coq_config.has_natdynlink then "true" else "false")