From c6753a3223389050af4059d0222e4efd9bda3b0f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 5 Sep 2014 18:22:15 +0200
Subject: Regression test for bug #2883.

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

diff --git a/test-suite/bugs/closed/2883.v b/test-suite/bugs/closed/2883.v
new file mode 100644
index 0000000000..5a5d90a403
--- /dev/null
+++ b/test-suite/bugs/closed/2883.v
@@ -0,0 +1,34 @@
+Require Import List.
+Require Import Coq.Program.Equality.
+
+Inductive star {genv state : Type}
+  (step : genv -> state -> state -> Prop)
+  (ge : genv) : state -> state -> Prop :=
+  | star_refl : forall s : state, star step ge s s
+  | star_step :
+    forall (s1 : state) (s2 : state)
+      (s3 : state),
+      step ge s1 s2 ->
+      star step ge s2 s3 ->
+      star step ge s1 s3.
+
+Parameter genv expr env mem : Type.
+Definition genv' := genv.
+Inductive state : Type :=
+ | State : expr -> env -> mem -> state.
+Parameter step : genv' -> state -> state -> Prop.
+
+Section Test.
+
+Variable ge : genv'.
+
+Lemma compat_eval_steps:
+  forall a b e a' b',
+  star step ge (State a e b) (State a' e b') ->
+  True.
+Proof.
+  intros. dependent induction H.
+  trivial.
+  eapply IHstar; eauto.
+  replace s2 with (State a' e b') by admit. eauto.
+Qed. (* Oups *)
-- 
cgit v1.2.3