Merge PR #9659: Fix #9652: rewrite fails to detect lack of progress

Ack-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: ppedrot

1 files changed, 19 insertions, 0 deletions

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.