aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqinit.ml3
1 files changed, 0 insertions, 3 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index a21e33c876..90a36620ab 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -98,7 +98,6 @@ let init_load_path () =
let coqlib = Envars.coqlib () in
let user_contrib = coqlib/"user-contrib" in
let dirs = "states" :: ["contrib"] in
- let camlp4 = Envars.camlp4lib () in
(* first user-contrib *)
if Sys.file_exists user_contrib then
Mltop.add_rec_path user_contrib Nameops.default_root_prefix;
@@ -110,8 +109,6 @@ let init_load_path () =
List.iter
(fun (s,alias) -> Mltop.add_rec_path (coqlib/s) (Names.make_dirpath [Names.id_of_string alias; Nameops.coq_root]))
theories_dirs_map;
- (* then camlp4lib *)
- add_ml_include camlp4;
(* then current directory *)
Mltop.add_path "." Nameops.default_root_prefix;
(* additional loadpath, given with -I -include -R options *)