From 67bef9f9b7be5415fbaad1e7b504aad7ec60a5e2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Glen=20M=C3=A9vel?= <glen.mevel@crans.org>
Date: Thu, 3 May 2018 12:05:45 +0200
Subject: [PATCH] fix `head_stuck`

---
 theories/program_logic/ectx_language.v | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 25a241279..7055956f1 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -101,7 +101,7 @@ Section ectx_language.
   Definition head_irreducible (e : expr Λ) (σ : state Λ) :=
     ∀ e' σ' efs, ¬head_step e σ e' σ' efs.
   Definition head_stuck (e : expr Λ) (σ : state Λ) :=
-    to_val e = None ∧ ∀ K e', e = fill K e' → head_irreducible e' σ.
+    to_val e = None ∧ head_irreducible e σ.
 
   (* All non-value redexes are at the root.  In other words, all sub-redexes are
      values. *)
@@ -168,9 +168,8 @@ Section ectx_language.
   Lemma head_stuck_stuck e σ :
     head_stuck e σ → sub_redexes_are_values e → stuck e σ.
   Proof.
-    move=>[] ? Hirr ?. split; first done.
-    apply prim_head_irreducible; last done.
-    apply (Hirr empty_ectx). by rewrite fill_empty.
+    intros [] ?. split; first done.
+    by apply prim_head_irreducible.
   Qed.
 
   Lemma ectx_language_atomic a e :
-- 
GitLab