From 54d2fa740258ceeb7575cae41f67fdb845e61c25 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 5 Jun 2018 10:22:31 +0200
Subject: [PATCH] remove base_logic/deprecated

Fixes #193
---
 _CoqProject                      |  1 -
 theories/base_logic/deprecated.v | 16 ----------------
 2 files changed, 17 deletions(-)
 delete mode 100644 theories/base_logic/deprecated.v

diff --git a/_CoqProject b/_CoqProject
index 906e22299..582ae30e9 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 e6cf27f42..000000000
--- 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.
-*)
-- 
GitLab