From 46f8eed8b082a074a426c9637e8fc201620f429f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 6 Dec 2016 20:48:09 +0100
Subject: [PATCH] =?UTF-8?q?Turn=20a=20~=20into=20a=20=C2=AC.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 program_logic/language.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/program_logic/language.v b/program_logic/language.v
index a1eff5564..de0d0a0c3 100644
--- a/program_logic/language.v
+++ b/program_logic/language.v
@@ -35,7 +35,7 @@ Section language.
   Definition reducible (e : expr Λ) (σ : state Λ) :=
     ∃ e' σ' efs, prim_step e σ e' σ' efs.
   Definition irreducible (e : expr Λ) (σ : state Λ) :=
-    ∀e' σ' efs, ~prim_step e σ e' σ' efs. 
+    ∀e' σ' efs, ¬prim_step e σ e' σ' efs. 
   Definition atomic (e : expr Λ) : Prop :=
     ∀ σ e' σ' efs, prim_step e σ e' σ' efs → irreducible e' σ'.
   Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
-- 
GitLab