diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 52d8ed704479c4156b92efbb9af8bfd7548b46a3..ba41b1898570fbaa64b031603b60e1da6a7271fb 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -244,6 +244,7 @@ Notation "(∧)" := bi_and (only parsing) : bi_scope.
 Infix "∨" := bi_or : bi_scope.
 Notation "(∨)" := bi_or (only parsing) : bi_scope.
 Infix "→" := bi_impl : bi_scope.
+Notation "¬ P" := (P → False)%I : bi_scope.
 Infix "∗" := bi_sep : bi_scope.
 Notation "(∗)" := bi_sep (only parsing) : bi_scope.
 Notation "P -∗ Q" := (bi_wand P Q) : bi_scope.