From aea3b3041bea042526e577f9a194efe83f6e7109 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 20 Jan 2016 00:43:11 +0100
Subject: [PATCH] Fix bug in step relation of language.

---
 iris/language.v | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/iris/language.v b/iris/language.v
index c92a7ebb9..b3aa860f2 100644
--- a/iris/language.v
+++ b/iris/language.v
@@ -34,13 +34,10 @@ Section language.
   Inductive step (ρ1 ρ2 : cfg) : Prop :=
     | step_atomic e1 σ1 e2 σ2 ef t1 t2 :
        ρ1 = (t1 ++ e1 :: t2, σ1) →
-       ρ1 = (t1 ++ e2 :: t2 ++ option_list ef, σ2) →
+       ρ2 = (t1 ++ e2 :: t2 ++ option_list ef, σ2) →
        prim_step e1 σ1 e2 σ2 ef →
        step ρ1 ρ2.
 
-  Definition steps := rtc step.
-  Definition stepn := nsteps step.
-
   Record is_ctx (K : E → E) := IsCtx {
     is_ctx_value e : to_val e = None → to_val (K e) = None;
     is_ctx_step_preserved e1 σ1 e2 σ2 ef :
-- 
GitLab