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).

1 files changed, 28 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/2900.v b/test-suite/bugs/closed/2900.v
new file mode 100644
index 000000000..8f4264e91
--- /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.