From 36dd5dba9c7a86ef97e9f8bd96cbf6340098e2b7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 1 Apr 2014 17:32:50 +0200
Subject: Fixing bug #2900 (evar/evar unif was supposed to be treated in
 solve_simple_eqn but in case the second evar was hidden behind a local
 variable, it arrived in evar_define and imitate, wrongly assuming progress).

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

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/2900.v b/test-suite/bugs/closed/2900.v
new file mode 100644
index 0000000000..8f4264e910
--- /dev/null
+++ b/test-suite/bugs/closed/2900.v
@@ -0,0 +1,28 @@
+(* Was raising stack overflow in 8.4 and assertion failed in future 8.5 *)
+Set Implicit Arguments.
+
+Require Import List.
+Require Import Coq.Program.Equality.
+
+(** Reflexive-transitive closure ( R* ) *)
+
+Inductive rtclosure (A : Type) (R : A-> A->Prop) : A->A->Prop :=
+  | rtclosure_refl : forall x,
+      rtclosure R x x
+  | rtclosure_step : forall y x z,
+      R x y -> rtclosure R y z -> rtclosure R x z.
+  (* bug goes away if rtclosure_step is commented out *)
+
+(** The closure of the trivial binary relation [eq] *)
+
+Definition tr (A:Type) := rtclosure (@eq A).
+
+(** The bug *)
+
+Lemma bug : forall A B (l t:list A) (r s:list B),
+    length l = length r ->
+    tr (combine l r) (combine t s) -> tr l t.
+Proof.
+  intros * E Hp.
+  (* bug goes away if [revert E] is called explicitly *)
+  dependent induction Hp.
-- 
cgit v1.2.3