aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-01 00:59:46 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-01 00:59:46 +0200
commit114d5f0d0bca9f01d7a5ab3381a9b9ca4291191a (patch)
tree3aeacfad3a11279599bf4362f8318eb2d8b62ccd /tools
parent842dfef1d52c739119808ea1dec3509c0cf86435 (diff)
parentd0a9edabf59a858625d11516cdb230d223a77aeb (diff)
Merge branch 'yet-another-makefile-bigbang' into trunk
Diffstat (limited to 'tools')
-rw-r--r--tools/compat5b.ml13
-rw-r--r--tools/coqdep_common.ml6
2 files changed, 3 insertions, 16 deletions
diff --git a/tools/compat5b.ml b/tools/compat5b.ml
deleted file mode 100644
index 37cb487c5..000000000
--- a/tools/compat5b.ml
+++ /dev/null
@@ -1,13 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* This file is meant for camlp5, for which there is nothing to
- add to gain camlp5 compatibility :-).
-
- See [compat5b.mlp] for the [camlp4] counterpart
-*)
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index c63e4aaa6..0f7937d72 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -9,11 +9,11 @@
open Printf
open Coqdep_lexer
open Unix
-open System
+open Minisys
(** [coqdep_boot] is a stripped-down version of [coqdep], whose
behavior is the one of [coqdep -boot]. Its only dependencies
- are [Coqdep_lexer] and [Unix], and it should stay so.
+ are [Coqdep_lexer], [Unix] and [Minisys], and it should stay so.
If it need someday some additional information, pass it via
options (see for instance [option_natdynlk] below).
*)
@@ -526,7 +526,7 @@ let rec add_directory recur add_file phys_dir log_dir =
| FileRegular f ->
add_file phys_dir log_dir f
in
- System.check_unix_dir (fun s -> eprintf "*** Warning: %s\n" s) phys_dir;
+ check_unix_dir (fun s -> eprintf "*** Warning: %s\n" s) phys_dir;
if exists_dir phys_dir then
process_directory f phys_dir
else