Skip to content
Snippets Groups Projects
Commit 4d7f63ca authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove type class instances that is now in Iris.

parent 5772761a
No related branches found
No related tags found
No related merge requests found
......@@ -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.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment