From f17096fa9eff103f40e6d381ebeb4313002fa378 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 24 Jan 2016 16:25:38 +0100
Subject: Fixing bug #4373: coqdep does not know about .vio files.

---
 tools/coqdep_common.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'tools')

diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 58c8e884cc..a90264e261 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -504,15 +504,15 @@ let add_caml_known phys_dir _ f =
     | _ -> ()
 
 let add_coqlib_known recur phys_dir log_dir f =
-  match get_extension f [".vo"] with
-    | (basename,".vo") ->
+  match get_extension f [".vo"; ".vio"] with
+    | (basename, (".vo" | ".vio")) ->
         let name = log_dir@[basename] in
         let paths = if recur then suffixes name else [name] in
         List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
     | _ -> ()
 
 let add_known recur phys_dir log_dir f =
-  match get_extension f [".v";".vo"] with
+  match get_extension f [".v"; ".vo"; ".vio"] with
     | (basename,".v") ->
 	let name = log_dir@[basename] in
 	let file = phys_dir//basename in
@@ -521,7 +521,7 @@ let add_known recur phys_dir log_dir f =
           let paths = List.tl (suffixes name) in
           let iter n = safe_hash_add compare_file clash_v vKnown (n, (file, false)) in
           List.iter iter paths
-    | (basename,".vo") when not(!option_boot) ->
+    | (basename, (".vo" | ".vio")) when not(!option_boot) ->
         let name = log_dir@[basename] in
 	let paths = if recur then suffixes name else [name] in
         List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
-- 
cgit v1.2.3


From 5361b02a96704a226b713b6040b67ca01de808fa Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 24 Jan 2016 18:00:34 +0100
Subject: Tentative fix for bug #4522: Incorrect "Warning..." on windows.

---
 tools/coq_makefile.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 478cf8875a..c4b7618270 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -99,7 +99,13 @@ let string_prefix a b =
 let is_prefix dir1 dir2 =
   let l1 = String.length dir1 in
   let l2 = String.length dir2 in
-    dir1 = dir2 || (l1 < l2 && String.sub dir2 0 l1 = dir1 && dir2.[l1] = '/')
+  let sep = Filename.dir_sep in
+  if dir1 = dir2 then true
+  else if l1 + String.length sep <= l2 then
+    let dir1' = String.sub dir2 0 l1 in
+    let sep' = String.sub dir2 l1 (String.length sep) in
+    dir1' = dir1 && sep' = sep
+  else false
 
 let physical_dir_of_logical_dir ldir =
   let le = String.length ldir - 1 in
-- 
cgit v1.2.3