From 53edf58bde7fca5c1492a259ea4b3ba147e73574 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 16 Feb 2016 11:31:43 +0100
Subject: [PATCH] Use unicode not for mkSet_not_elem_of.

---
 prelude/sets.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/prelude/sets.v b/prelude/sets.v
index ddd3a3cb2..bd8e98deb 100644
--- a/prelude/sets.v
+++ b/prelude/sets.v
@@ -20,7 +20,7 @@ Proof. by split; [split | |]; repeat intro. Qed.
 
 Lemma mkSet_elem_of {A} (f : A → Prop) x : f x → x ∈ mkSet f.
 Proof. done. Qed.
-Lemma mkSet_not_elem_of {A} (f : A → Prop) x : ~f x → x ∉ mkSet f.
+Lemma mkSet_not_elem_of {A} (f : A → Prop) x : ¬f x → x ∉ mkSet f.
 Proof. done. Qed.
 
 Instance set_ret : MRet set := λ A (x : A), {[ x ]}.
-- 
GitLab