From 82a75fc2e2ef7a9716d38465a903199607f9b8aa Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 1 Oct 2020 13:46:29 +0200
Subject: [PATCH] ASCII notation for negation in bi_scope.

---
 theories/bi/ascii.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/bi/ascii.v b/theories/bi/ascii.v
index 159f0b964..52ec4bebf 100644
--- a/theories/bi/ascii.v
+++ b/theories/bi/ascii.v
@@ -31,6 +31,8 @@ Notation "(/\)" := bi_and (only parsing) : bi_scope.
 Notation "P \/ Q" := (P ∨ Q)%I (only parsing) : bi_scope.
 Notation "(\/)" := bi_or (only parsing) : bi_scope.
 Notation "P -> Q" := (P → Q)%I (only parsing) : bi_scope.
+Notation "~ P" := (P → False)%I (only parsing) : bi_scope.
+
 Notation "P ** Q" := (P ∗ Q)%I
   (at level 80, right associativity, only parsing) : bi_scope.
 Notation "(**)" := bi_sep (only parsing) : bi_scope.
-- 
GitLab