diff --git a/theories/bi/ascii.v b/theories/bi/ascii.v
index 159f0b964a07c0fb761f84afc934f1f3048b1cee..52ec4bebf2dd7d0fab0891695108aac0bb37336b 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.