Coqdep always uses / as dir_sep

5 files changed, 19 insertions, 11 deletions

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index bd77bb1bae..bf2a091801 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -331,7 +331,7 @@ let implicit () =
     print "%.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
     print "%.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
     print "%.ml4.d: %.ml4\n";
-    print "\t$(COQDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
+    print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
   let ml_rules () =
     print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
     print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
@@ -344,12 +344,12 @@ let implicit () =
     print "%.cma: | %.mllib\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
     print "%.cmxa: | %.mllib\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
     print "%.mllib.d: %.mllib\n";
-    print "\t$(COQDEP) -slash $(COQLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
+    print "\t$(COQDEP) $(COQLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
   let mlpack_rules () =
     print "%.cmo: | %.mlpack\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n";
     print "%.cmx: | %.mlpack\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n";
     print "%.mlpack.d: %.mlpack\n";
-    print "\t$(COQDEP) -slash $(COQLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
+    print "\t$(COQDEP) $(COQLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
 in
   let v_rules () =
     print "%.vo %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
@@ -360,7 +360,7 @@ in
     print "%.g.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@\n\n";
     print "%.g.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS)  -html -g $< -o $@\n\n";
     print "%.v.d: %.v\n";
-    print "\t$(COQDEP) -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
+    print "\t$(COQDEP) $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
     print "%.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*\n\n"
   in
     if !some_mlifile then mli_rules ();
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 16e5bbde8d..8a514f7f43 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -184,7 +184,9 @@ let rec parse = function
   | "-coqlib" :: [] -> usage ()
   | "-suffix" :: s :: ll -> suffixe := s ; parse ll
   | "-suffix" :: [] -> usage ()
-  | "-slash" :: ll -> option_slash := true; parse ll
+  | "-slash" :: ll ->
+    Printf.eprintf "warning: option -slash has no effect and is deprecated.";
+    parse ll
   | ("-h"|"--help"|"-help") :: _ -> usage ()
   | f :: ll -> treat_file None f; parse ll
   | [] -> ()
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index 15fcdc6009..588bf2dcf1 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -16,7 +16,6 @@ open Coqdep_common
 *)
 
 let rec parse = function
-  | "-slash" :: ll -> option_slash := true; parse ll
   | "-natdynlink" :: "no" :: ll -> option_natdynlk := false; parse ll
   | "-c" :: ll -> option_c := true; parse ll
   | "-boot" :: ll -> parse ll (* We're already in boot mode by default *)
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 8c5e5b1ee4..759b0cf967 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -22,7 +22,6 @@ let stdout = Pervasives.stdout
 
 let option_c = ref false
 let option_noglob = ref false
-let option_slash = ref false
 let option_natdynlk = ref true
 let option_mldep = ref None
 
@@ -33,9 +32,18 @@ let suffixe = ref ".vo"
 
 type dir = string option
 
-(* filename for printing *)
-let (//) s1 s2 =
-  if !option_slash then s1^"/"^s2 else Filename.concat s1 s2
+(* Filename.concat but always with a '/' *)
+let is_dir_sep s i =
+  match Sys.os_type with
+  | "Unix" -> s.[i] = '/'
+  | "Cygwin" | "Win32" ->
+    let c = s.[i] in c = '/' || c = '\\' || c = ':'
+
+let (//) dirname filename =
+  let l = String.length dirname in
+  if l = 0 || is_dir_sep dirname (l-1)
+  then dirname ^ filename
+  else dirname ^ "/" ^ filename
 
 (** [get_extension f l] checks whether [f] has one of the extensions
     listed in [l]. It returns [f] without its extension, alongside with
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index d9ca3ca819..37be010ead 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -8,7 +8,6 @@
 
 val option_c : bool ref
 val option_noglob : bool ref
-val option_slash : bool ref
 val option_natdynlk : bool ref
 val option_mldep : string option ref
 val norec_dirs : string list ref