From 4d7f63cad71459e56c71752c13d445cad13ae9f9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 28 Nov 2016 10:16:35 +0100
Subject: [PATCH] Remove type class instances that is now in Iris.

---
 theories/lifetime/rebor.v | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/theories/lifetime/rebor.v b/theories/lifetime/rebor.v
index 3dabd333..5311c81d 100644
--- a/theories/lifetime/rebor.v
+++ b/theories/lifetime/rebor.v
@@ -4,10 +4,6 @@ From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
 
-Global Instance into_wand_bupd {M} (R P Q : uPred M) :
-  IntoWand R P Q → IntoWand R (▷ P) (▷ Q) | 100.
-Proof. rewrite /IntoWand=>->. Admitted.
-
 Section rebor.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
-- 
GitLab