From a4db087565dd2ecfa3bcc022277bed1a3c868fd3 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 11 Jun 2014 17:19:14 +0200
Subject: Fix bug #3291, stack overflow in rewrite.

---
 test-suite/bugs/opened/3291.v | 8 --------
 1 file changed, 8 deletions(-)
 delete mode 100644 test-suite/bugs/opened/3291.v

(limited to 'test-suite/bugs/opened')

diff --git a/test-suite/bugs/opened/3291.v b/test-suite/bugs/opened/3291.v
deleted file mode 100644
index 4e1c2630e3..0000000000
--- a/test-suite/bugs/opened/3291.v
+++ /dev/null
@@ -1,8 +0,0 @@
-Require Import Setoid.
-
-Definition segv : forall x, (x = 0%nat) -> (forall (y : nat), (y < x)%nat -> nat) = forall (y : nat), (y < 0)%nat -> nat.
-intros x eq.
-assert (H : forall y, (y < x)%nat = (y < 0)%nat).
-rewrite -> eq. auto.
-Fail Timeout 1 setoid_rewrite <- H. (* The command has indeed failed with message:
-=> Stack overflow. *)
-- 
cgit v1.2.3