From 1d769e02b3baba54246c942fe116abaf850892db Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 24 Oct 2016 11:44:24 +0200
Subject: Fix 6d5fe92e to #5150 (missing dependencies in test suite) was a bit
 too strong.

New fix. A bit less consistent with the spirit of this Makefile as we
list prerequisite files explicitly, but avoid to redo subsystems at
each call to "make" as with previous fix.

Other solutions from experts are welcome.
---
 test-suite/Makefile | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 8500ef1b3d..491b16960e 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -84,6 +84,9 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
 # All subsystems
 SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk
 
+PREREQUISITELOG = prerequisite/admit.v.log			\
+  prerequisite/make_local.v.log prerequisite/make_notation.v.log
+
 #######################################################################
 # Phony targets
 #######################################################################
@@ -221,7 +224,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
 	  fi; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v prerequisite
+$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \
@@ -253,7 +256,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v
 	  fi; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v prerequisite
+$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -267,7 +270,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v prerequisite
 	  fi; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out prerequisite
+$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -289,7 +292,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out prerequisite
 	  rm $$tmpoutput; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v prerequisite
+$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -307,7 +310,7 @@ $(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v prerequisite
 # the .v file with exactly two digits after the dot. The reference for
 # time is a 6120 bogomips cpu.
 ifneq (,$(bogomips))
-$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v prerequisite
+$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -338,7 +341,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v prerequisite
 endif
 
 # Ideal-features tests
-$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v prerequisite
+$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-- 
cgit v1.2.3


From 5f1dd4c401110d6b10350c847805c6923fa09de5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 24 Oct 2016 17:04:41 +0200
Subject: Fixing #3479 (parsing of "{" and "}" when a keyword starts with "{"
 or "}").

---
 test-suite/success/Notations.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 2f7c62972a..511b60b4bb 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -110,3 +110,9 @@ Goal True -> True. intros H. exact H. Qed.
 
 (* Check absence of collision on ".." in nested notations with ".." *)
 Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)).
+
+(* Check parsing of { and } is not affected by notations #3479 *)
+Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10).
+Goal True.
+{{ exact I. }}
+Qed.
-- 
cgit v1.2.3