6 files changed, 21 insertions, 32 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 6efd47afc2..ba591ede20 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -317,8 +317,6 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
 	    echo "    $<...correctly prepared" ; \
 	  fi; \
 	} > "$@"
-	@echo "CHECK     $<"
-	$(HIDE)$(coqchk) -norec TestSuite.$(shell basename $< .v) > $(shell dirname $<)/$(shell basename $< .v).chk.log 2>&1
 
 ssr: $(wildcard ssr/*.v:%.v=%.v.log)
 $(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v arithmetic/*.v)): %.v.log: %.v $(PREREQUISITELOG)
diff --git a/test-suite/bugs/closed/bug_9595.v b/test-suite/bugs/closed/bug_9595.v
new file mode 100644
index 0000000000..312ed7d045
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9595.v
@@ -0,0 +1,11 @@
+Set Primitive Projections.
+Set Warnings "+non-primitive-record".
+
+(* 0 fields *)
+Fail Record foo := { a := 0 }.
+
+(* anonymous field *)
+Fail Record foo := { _ : nat }.
+
+(* squashed *)
+Fail Record foo : Prop := { a : nat }.
diff --git a/test-suite/bugs/closed/bug_9631.v b/test-suite/bugs/closed/bug_9631.v
new file mode 100644
index 0000000000..8afeccccd4
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9631.v
@@ -0,0 +1,7 @@
+
+Fail Instance x : _.
+
+Existing Class True.
+(* the type is checked for typeclass-ness before interping the body so
+   this is the same error *)
+Fail Instance x : _ := I.
diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v
deleted file mode 100644
index b7c98aa134..0000000000
--- a/test-suite/output-modulo-time/ltacprof_cutoff.v
+++ /dev/null
@@ -1,28 +0,0 @@
-(* -*- coq-prog-args: ("-async-proofs" "off" "-profile-ltac") -*- *)
-Require Coq.ZArith.BinInt.
-Module WithIdTac.
-  Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac).
-
-  Ltac foo0 := idtac; sleep.
-  Ltac foo1 := sleep; foo0.
-  Ltac foo2 := sleep; foo1.
-  Goal True.
-    foo2.
-    Show Ltac Profile CutOff 47.
-    constructor.
-  Qed.
-End WithIdTac.
-
-Module TestEval.
-  Ltac sleep := let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac.
-
-  Ltac foo0 := idtac; do 50 (idtac; sleep).
-  Ltac foo1 := sleep; foo0.
-  Ltac foo2 := sleep; foo1.
-  Goal True.
-    Reset Ltac Profile.
-    foo2.
-    Show Ltac Profile CutOff 47.
-    constructor.
-  Qed.
-End TestEval.
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index ba4bc070c6..3f0717666c 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -113,7 +113,8 @@ Sequences of implicit arguments must be of different lengths.
 The command has indeed failed with message:
 Some argument names are duplicated: F
 The command has indeed failed with message:
-Argument z cannot be declared implicit.
+Argument number 2 (anonymous in original definition) cannot be declared
+implicit.
 The command has indeed failed with message:
 Extra arguments: y.
 The command has indeed failed with message:
diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v
index d7c271c3ec..d95cc0e32f 100644
--- a/test-suite/output/PrintInfos.v
+++ b/test-suite/output/PrintInfos.v
@@ -22,7 +22,7 @@ Print comparison.
 Definition foo := forall x, x = 0.
 Parameter bar : foo.
 
-Arguments bar [x].
+Arguments bar {x}.
 About bar.
 Print bar.