From bf840bafc19deba67e5270dfd31b8b6662b73132 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 26 Feb 2019 23:41:38 +0100
Subject: Fix #9652: rewrite fails to detect lack of progress

---
 test-suite/bugs/closed/bug_9652.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_9652.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3