5 files changed, 36 insertions, 6 deletions
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,$<); \
diff --git a/test-suite/bugs/closed/5127.v b/test-suite/bugs/closed/5127.v
new file mode 100644
index 0000000000..831e8fb507
--- /dev/null
+++ b/test-suite/bugs/closed/5127.v
@@ -0,0 +1,15 @@
+Fixpoint arrow (n: nat) :=
+  match n with
+  | S n => bool -> arrow n
+  | O => bool
+  end.
+
+Fixpoint apply (n : nat) : arrow n -> bool :=
+  match n return arrow n -> bool with
+  | S n => fun f => apply _ (f true)
+  | O => fun x => x
+  end.
+
+Axiom f : arrow 10000.
+Definition v : bool := Eval compute in apply _ f.
+Definition w : bool := Eval vm_compute in v.
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index d003c70df9..266e4c7243 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -1,2 +1,3 @@
 The command has indeed failed with message:
 Error: Ltac variable y depends on pattern variable name z which is not bound in current context.
+Hx
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 7e2610c7d7..e5bcff8ddb 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -15,3 +15,8 @@ lazymatch goal with
 | H1 : HT |- _ => idtac
 end.
 Abort.
+
+(* Check printing of the "var" argument "Hx" *)
+Ltac m H := idtac H; exact H.
+Goal True.
+let a:=constr:(let Hx := 0 in ltac:(m Hx)) in idtac.
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.