9 files changed, 35 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/2969.v b/test-suite/bugs/closed/2969.v
index a03adbd73c..7b1a261789 100644
--- a/test-suite/bugs/closed/2969.v
+++ b/test-suite/bugs/closed/2969.v
@@ -12,6 +12,7 @@ eexists.
 reflexivity.
 Grab Existential Variables.
 admit.
+Admitted.
 
 (* Alternative variant which failed but without raising anomaly *)
 
@@ -24,3 +25,4 @@ clearbody n n0.
 exact I.
 Grab Existential Variables.
 admit.
+Admitted.
diff --git a/test-suite/bugs/closed/3377.v b/test-suite/bugs/closed/3377.v
index 8e9e3933cc..abfcf1d355 100644
--- a/test-suite/bugs/closed/3377.v
+++ b/test-suite/bugs/closed/3377.v
@@ -5,6 +5,7 @@ Record prod A B := pair { fst : A; snd : B}.
 Goal fst (@pair Type Type Type Type).
 Set Printing All.
 match goal with |- ?f ?x => set (foo := f x) end.
+Abort.
 
 Goal forall x : prod Set Set, x = @pair _ _ (fst x) (snd x).
 Proof.
@@ -12,6 +13,6 @@ Proof.
   lazymatch goal with
     | [ |- ?x = @pair _ _ (?f ?x) (?g ?x) ] => pose f
   end.
-
 (* Toplevel input, characters 7-44:
 Error: No matching clauses for match. *)
+Abort.
diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v
index 606c6e0845..668f6bb428 100644
--- a/test-suite/bugs/closed/4069.v
+++ b/test-suite/bugs/closed/4069.v
@@ -41,6 +41,8 @@ Proof. f_equal.
   8.5: 2 goals, skipn n l = l -> k ++ skipn n l = skipn n l
     and skipn n l = l
 *)
+Abort.
+
 Require Import List.
 Fixpoint replicate {A} (n : nat) (x : A) : list A :=
   match n with 0 => nil | S n => x :: replicate n x end.
diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v
index eb37141bcf..28800ac05a 100644
--- a/test-suite/bugs/closed/4198.v
+++ b/test-suite/bugs/closed/4198.v
@@ -13,6 +13,7 @@ Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'),
   match goal with
     | [ |- context G[@hd] ] => idtac
   end.
+Abort.
 
 (* This second example comes from CFGV where inspecting subterms of a
    match is expecting to inspect first the term to match (even though
@@ -35,3 +36,4 @@ Ltac mydestruct :=
 Goal forall x, match x with 0 => 0 | _ => 0 end = 0.
 intros.
 mydestruct.
+Abort.
diff --git a/test-suite/bugs/closed/4722.v b/test-suite/bugs/closed/4722.v
deleted file mode 100644
index 2d41828f19..0000000000
--- a/test-suite/bugs/closed/4722.v
+++ /dev/null
@@ -1 +0,0 @@
-(* -*- coq-prog-args: ("-R" "4722" "Foo") -*- *)
diff --git a/test-suite/bugs/closed/4722/tata b/test-suite/bugs/closed/4722/tata
deleted file mode 120000
index b38e66e75f..0000000000
--- a/test-suite/bugs/closed/4722/tata
+++ /dev/null
@@ -1 +0,0 @@
-toto
-\ No newline at end of file
diff --git a/test-suite/bugs/closed/4782.v b/test-suite/bugs/closed/4782.v
index dbd71035dc..1e1a4cb9c2 100644
--- a/test-suite/bugs/closed/4782.v
+++ b/test-suite/bugs/closed/4782.v
@@ -6,6 +6,7 @@ Inductive p : Prop := consp : forall (e : r) (x : type e), cond e x -> p.
 
 Goal p.
 Fail apply consp with (fun _ : bool => mk_r unit (fun x => True)) nil.
+Abort.
  
 (* A simplification of an example from coquelicot, which was failing
    at some time after a fix #4782 was committed. *)
@@ -21,4 +22,5 @@ Set Typeclasses Debug.
 Goal forall (A:T) (x:dom A), pairT A A = pairT A A.
 intros.
 apply (F _ _)  with (x,x).
+Abort.
   
diff --git a/test-suite/bugs/closed/7462.v b/test-suite/bugs/closed/7462.v
new file mode 100644
index 0000000000..40ca39e38a
--- /dev/null
+++ b/test-suite/bugs/closed/7462.v
@@ -0,0 +1,13 @@
+(* Adding an only-printing notation should not override existing
+   interpretations for the same notation. *)
+
+Notation "$ x" := (@id nat x) (only parsing, at level 0).
+Notation "$ x" := (@id bool x) (only printing, at level 0).
+Check $1. (* Was: Error: Unknown interpretation for notation "$ _". *)
+
+(* Adding an only-printing notation should not let believe
+   that a parsing rule has been given *)
+
+Notation "$ x" := (@id bool x) (only printing, at level 0).
+Notation "$ x" := (@id nat x) (only parsing, at level 0).
+Check $1. (* Was: Error: Syntax Error: Lexer: Undefined token *)
diff --git a/test-suite/bugs/closed/7554.v b/test-suite/bugs/closed/7554.v
new file mode 100644
index 0000000000..12b0aa2cb5
--- /dev/null
+++ b/test-suite/bugs/closed/7554.v
@@ -0,0 +1,12 @@
+Require Import Coq.Program.Tactics.
+
+(* these should not result in anomalies *)
+
+Fail Program Lemma foo:
+  forall P, forall H, forall (n:nat), P n.
+
+Fail Program Lemma foo:
+  forall a (P : list a -> Prop), forall H, forall (n:list a), P n.
+
+Fail Program Lemma foo:
+  forall (a : Type) (P : list a -> Prop), forall H, forall (n:list a), P n.