5 files changed, 54 insertions, 11 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index e3800ee22e..efa0236c35 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -51,7 +51,7 @@ SINGLE_QUOTE="
 get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_args,$(1)), ($(call get_coq_prog_args,$(1)))))
 # get the command to use with this set of arguments; if there's -compile, use coqc, else use coqtop
 has_compile_flag = $(filter "-compile",$(call get_coq_prog_args,$(1)))
-has_profile_ltac_or_compile_flag = $(filter "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1)))
+has_profile_ltac_or_compile_flag = $(filter "-profile-ltac-cutoff" "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1)))
 get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqc),$(command))
 
 
@@ -281,6 +281,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out
 	    | grep -v "\[Loading ML file" \
 	    | grep -v "Skipping rcfile loading" \
 	    | grep -v "^<W>" \
+	    | sed 's/File "[^"]*"/File "stdin"/' \
 	    > $$tmpoutput; \
 	  diff -u $*.out $$tmpoutput 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
diff --git a/test-suite/bugs/closed/4762.v b/test-suite/bugs/closed/4762.v
new file mode 100644
index 0000000000..7a87b07a8e
--- /dev/null
+++ b/test-suite/bugs/closed/4762.v
@@ -0,0 +1,24 @@
+Inductive myand (P Q : Prop) := myconj : P -> Q -> myand P Q.
+
+Lemma foo P Q R : R = myand P Q -> P -> Q -> R.
+Proof. intros ->; constructor; auto. Qed.
+
+Hint Extern 0 (myand _ _) => eapply foo; [reflexivity| |] : test1.
+
+Goal forall P Q R : Prop, P -> Q -> R -> myand P (myand Q R).
+Proof.
+  intros.
+  eauto with test1.
+Qed.
+
+Hint Extern 0 =>
+  match goal with
+  | |- myand _ _ => eapply foo; [reflexivity| |]
+  end : test2.
+
+Goal forall P Q R : Prop, P -> Q -> R -> myand P (myand Q R).
+Proof.
+  intros.
+  eauto with test2. (* works *)
+Qed.
+
diff --git a/test-suite/bugs/closed/4869.v b/test-suite/bugs/closed/4869.v
new file mode 100644
index 0000000000..6d21b66fe9
--- /dev/null
+++ b/test-suite/bugs/closed/4869.v
@@ -0,0 +1,18 @@
+Universes i.
+
+Fail Constraint i < Set.
+Fail Constraint i <= Set.
+Fail Constraint i = Set.
+Constraint Set <= i.
+Constraint Set < i.
+Fail Constraint i < j. (* undeclared j *)
+Fail Constraint i < Type. (* anonymous *)
+
+Set Universe Polymorphism.
+
+Section Foo.
+  Universe j.
+  Constraint Set < j.
+
+  Definition foo := Type@{j}.
+End Foo.
+\ No newline at end of file
diff --git a/test-suite/output-modulo-time/ltacprof.v b/test-suite/output-modulo-time/ltacprof.v
index d79451f0f7..6611db70e2 100644
--- a/test-suite/output-modulo-time/ltacprof.v
+++ b/test-suite/output-modulo-time/ltacprof.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs" "-profile-ltac") -*- *)
+(* -*- coq-prog-args: ("-emacs" "-profile-ltac-cutoff" "0.0") -*- *)
 Ltac sleep' := do 100 (do 100 (do 100 idtac)).
 Ltac sleep := sleep'.
 
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 815305581c..1633ad9765 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,20 +1,20 @@
-File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 1, characters 0-36:
+File "stdin", line 1, characters 0-36:
 Warning: Ignoring rename of x into y. Only implicit arguments can be renamed.
-[arguments-assert,vernacular]
+[arguments-ignore-rename-nonimpl,vernacular]
 The command has indeed failed with message:
 Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to B.
-File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 2, characters 0-25:
+File "stdin", line 2, characters 0-25:
 Warning: Ignoring rename of A into T. Only implicit arguments can be renamed.
-[arguments-assert,vernacular]
-File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 2, characters 0-25:
+[arguments-ignore-rename-nonimpl,vernacular]
+File "stdin", line 2, characters 0-25:
 Warning: This command is just asserting the number and names of arguments of
 identity. If this is what you want add ': assert' to silence the warning. If
 you want to clear implicit arguments add ': clear implicits'. If you want to
 clear notation scopes add ': clear scopes' [arguments-assert,vernacular]
-File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 4, characters 0-40:
+File "stdin", line 4, characters 0-40:
 Warning: Ignoring rename of x into y. Only implicit arguments can be renamed.
-[arguments-assert,vernacular]
+[arguments-ignore-rename-nonimpl,vernacular]
 @eq_refl
      : forall (B : Type) (y : B), y = y
 eq_refl
@@ -121,9 +121,9 @@ The command has indeed failed with message:
 Error: Argument z cannot be declared implicit.
 The command has indeed failed with message:
 Error: Extra argument y.
-File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 53, characters 0-26:
+File "stdin", line 53, characters 0-26:
 Warning: Ignoring rename of x into s. Only implicit arguments can be renamed.
-[arguments-assert,vernacular]
+[arguments-ignore-rename-nonimpl,vernacular]
 The command has indeed failed with message:
 Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to R.