diff --git a/_CoqProject b/_CoqProject
index 906e2229907957fc72e09c3ce21edd29ba4068cb..582ae30e99b1093d48784ab918f0eaaab6ec6308 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -48,7 +48,6 @@ theories/base_logic/derived.v
 theories/base_logic/base_logic.v
 theories/base_logic/soundness.v
 theories/base_logic/double_negation.v
-theories/base_logic/deprecated.v
 theories/base_logic/lib/iprop.v
 theories/base_logic/lib/own.v
 theories/base_logic/lib/saved_prop.v
diff --git a/theories/base_logic/deprecated.v b/theories/base_logic/deprecated.v
deleted file mode 100644
index e6cf27f42f870b11511531fa887fdc01e2fc1d7b..0000000000000000000000000000000000000000
--- a/theories/base_logic/deprecated.v
+++ /dev/null
@@ -1,16 +0,0 @@
-(*
-FIXME
-
-From iris.base_logic Require Import primitive.
-Set Default Proof Using "Type".
-
-(* Deprecated 2016-11-22. Use ⌜φ⌝ instead. *)
-Notation "■ φ" := (uPred_pure φ%stdpp%type)
-    (at level 20, right associativity, only parsing) : uPred_scope.
-
-(* Deprecated 2016-11-22. Use ⌜x = y⌝ instead. *)
-Notation "x = y" := (uPred_pure (x%stdpp%type = y%stdpp%type)) (only parsing) : uPred_scope.
-
-(* Deprecated 2016-11-22. Use ⌜x ## y ⌝ instead. *)
-Notation "x ## y" := (uPred_pure (x%stdpp%type ## y%stdpp%type)) (only parsing) : uPred_scope.
-*)