From 1d637f15de540c82289d6b3a16181a625a0d9cdf Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 4 Nov 2016 13:28:08 +0100
Subject: Fix #4837: ./configure -local makes coqdep issue many warnings

We simply remove the warnings about paths mixing Win32 and Unix
separators, since that situation does not seem problematic (c.f.
discussion on the bug tracker).
---
 tools/coqdep_common.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index cc63c13d7b..0064aebdae 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -526,7 +526,6 @@ let rec add_directory recur add_file phys_dir log_dir =
     | FileRegular f ->
         add_file phys_dir log_dir f
   in
-  check_unix_dir (fun s -> eprintf "*** Warning: %s\n" s) phys_dir;
   if exists_dir phys_dir then
     process_directory f phys_dir
   else
-- 
cgit v1.2.3


From 81c9fa0de99400b51c029cdbd1519b4f724e320a Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 17 Nov 2016 13:06:07 +0100
Subject: fake_ide: use the now available Status XML message

---
 tools/fake_ide.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'tools')

diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 8fcca535d1..214dfb4703 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -266,11 +266,9 @@ let eval_print l coq =
       let to_id, _ = get_id id in
       eval_call (query (phrase, to_id)) coq
   | [ Tok(_,"WAIT") ] ->
-      let phrase = "Stm Wait." in
-      eval_call (query (phrase,tip_id())) coq
+      eval_call (status false) coq
   | [ Tok(_,"JOIN") ] ->
-      let phrase = "Stm JoinDocument." in
-      eval_call (query (phrase,tip_id())) coq
+      eval_call (status true) coq
   | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] ->
       let to_id, _ = get_id id in
       if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip"
-- 
cgit v1.2.3


From 954f1697fb750eecf4612bbb191a91c3a4bafb7c Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 18 Nov 2016 08:38:12 +0100
Subject: Revert "fake_ide: use the now available Status XML message"

This reverts commit 81c9fa0de99400b51c029cdbd1519b4f724e320a.
---
 tools/fake_ide.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'tools')

diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 214dfb4703..8fcca535d1 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -266,9 +266,11 @@ let eval_print l coq =
       let to_id, _ = get_id id in
       eval_call (query (phrase, to_id)) coq
   | [ Tok(_,"WAIT") ] ->
-      eval_call (status false) coq
+      let phrase = "Stm Wait." in
+      eval_call (query (phrase,tip_id())) coq
   | [ Tok(_,"JOIN") ] ->
-      eval_call (status true) coq
+      let phrase = "Stm JoinDocument." in
+      eval_call (query (phrase,tip_id())) coq
   | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] ->
       let to_id, _ = get_id id in
       if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip"
-- 
cgit v1.2.3


From 102d2db3ea7a7354de5e019224e2778fe7603b8e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 21 Nov 2016 07:25:30 +0100
Subject: Stop parsing -compat-notations options, which are no longer supported
 (bug #3339).

---
 tools/coqc.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coqc.ml b/tools/coqc.ml
index b59bbdb1e0..b12d48710f 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -94,7 +94,6 @@ let parse_args () =
       |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"
       |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs"
       |"-impredicative-set"|"-vm"|"-native-compiler"
-      |"-verbose-compat-notations"|"-no-compat-notations"
       |"-indices-matter"|"-quick"|"-type-in-type"
       |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch"
       as o) :: rem ->
-- 
cgit v1.2.3


From aa86963464045d61fa0eaf3a7fe67ced7a6a73f4 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 21 Nov 2016 12:49:17 +0100
Subject: Remove spurious spaces in merlin file generated by coq_makefile (bug
 #5213).

---
 tools/coq_makefile.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index ac69a69a4a..eab909f5b1 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -887,7 +887,7 @@ let merlin targets (ml_inc,_,_) =
   print ".merlin:\n";
   print "\t@echo 'FLG -rectypes' > .merlin\n" ;
   List.iter (fun c ->
-      printf "\t@echo \"B $(COQLIB) %s\" >> .merlin\n" c)
+      printf "\t@echo \"B $(COQLIB)%s\" >> .merlin\n" c)
     lib_dirs ;
   List.iter (fun (_,c) ->
       printf "\t@echo \"B %s\" >> .merlin\n" c;
-- 
cgit v1.2.3


From 9568a34f665a6f3dca06271ffd6e914d9bd2a5ad Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 13 Jan 2017 08:42:13 +0100
Subject: Properly remove aux files in subdirectories (bug #5089).

The aux file for foo/bar.v is foo/.bar.aux, not .foo/bar.aux.
---
 tools/coq_makefile.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index eab909f5b1..b7dd5f2a14 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -390,7 +390,7 @@ let clean sds sps =
   let () =
     if !some_vfile then
       let () = print "cleanall:: clean\n" in
-      print "\trm -f $(patsubst %.v,.%.aux,$(VFILES))\n\n" in
+      print "\trm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux)\n\n" in
   print "archclean::\n";
   print "\trm -f *.cmx *.o\n";
   List.iter
-- 
cgit v1.2.3