4 files changed, 22 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/bug_4527.v b/test-suite/bugs/closed/bug_4527.v
index 4f8a8dd272..dfb07520f1 100644
--- a/test-suite/bugs/closed/bug_4527.v
+++ b/test-suite/bugs/closed/bug_4527.v
@@ -10,6 +10,7 @@ Inductive False := .
 Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
 Require Coq.Init.Datatypes.
+Require Import Coq.Init.Tactics.
 
 Import Coq.Init.Notations.
 
diff --git a/test-suite/bugs/closed/bug_4798.v b/test-suite/bugs/closed/bug_4798.v
index 696812dee1..f238086633 100644
--- a/test-suite/bugs/closed/bug_4798.v
+++ b/test-suite/bugs/closed/bug_4798.v
@@ -1,5 +1,5 @@
 (* DO NOT MODIFY THIS FILE DIRECTLY *)
 (* It is autogenerated by dev/tools/update-compat.py. *)
 Check match 2 with 0 => 0 | S n => n end.
-Notation "|" := 1 (compat "8.7").
+Notation "|" := 1 (compat "8.8").
 Check match 2 with 0 => 0 | S n => n end. (* fails *)
diff --git a/test-suite/bugs/closed/bug_9166.v b/test-suite/bugs/closed/bug_9166.v
index a89837dd12..21cd770cbb 100644
--- a/test-suite/bugs/closed/bug_9166.v
+++ b/test-suite/bugs/closed/bug_9166.v
@@ -2,7 +2,7 @@
 (* It is autogenerated by dev/tools/update-compat.py. *)
 Set Warnings "+deprecated".
 
-Notation bar := option (compat "8.7").
+Notation bar := option (compat "8.8").
 
 Definition foo (x: nat) : nat :=
   match x with
diff --git a/test-suite/bugs/closed/bug_9652.v b/test-suite/bugs/closed/bug_9652.v
new file mode 100644
index 0000000000..21ce1bea61
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9652.v
@@ -0,0 +1,19 @@
+Set Universe Polymorphism.
+Require Import Coq.ZArith.BinInt.
+Class word_interface (width : Z) : Type := Build_word
+  { rep : Type;
+    unsigned : rep -> Z;
+    of_Z : Z -> rep;
+    sub : rep -> rep -> rep }.
+Coercion rep : word_interface >-> Sortclass.
+Axiom word : word_interface 64. Local Existing Instance word.
+Goal
+  forall (x : list word) (x1 x2 : word),
+  (unsigned (sub x2 x1) / 2 ^ 4 * 2 ^ 3 <
+   unsigned (of_Z 8) * Z.of_nat (Datatypes.length x))%Z.
+Proof.
+  intros.
+  assert (unsigned (sub x2 x1) = unsigned (sub x2 x1)) by exact eq_refl.
+  Fail progress rewrite H.
+  Fail rewrite H.
+Abort.