From 4973d0b3788b96788ec88c299490f11f081bc667 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 23 Dec 2020 10:57:34 +0100
Subject: [PATCH] Remove old `Hint Extern` hack for `impl_persistent` that
 seems no longer needed.

---
 iris/bi/plainly.v | 10 +---------
 tests/bi.ref      |  0
 tests/bi.v        |  9 +++++++++
 3 files changed, 10 insertions(+), 9 deletions(-)
 create mode 100644 tests/bi.ref
 create mode 100644 tests/bi.v

diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index aa9906ef6..a58399996 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -362,8 +362,7 @@ Proof. intros; destruct p; simpl; apply _. Qed.
 Lemma plain_persistent P : Plain P → Persistent P.
 Proof. intros. by rewrite /Persistent -plainly_elim_persistently. Qed.
 
-(* Not an instance, see the bottom of this file *)
-Lemma impl_persistent P Q :
+Global Instance impl_persistent P Q :
   Absorbing P → Plain P → Persistent Q → Persistent (P → Q).
 Proof.
   intros. by rewrite /Persistent {2}(plain P) -persistently_impl_plainly
@@ -645,10 +644,3 @@ To avoid that, we declare it using a [Hint Immediate], so that it will
 only be used at the leaves of the proof search tree, i.e. when the
 premise of the hint can be derived from just the current context. *)
 Global Hint Immediate plain_persistent : typeclass_instances.
-
-(* Not defined using an ordinary [Instance] because the default
-[class_apply @impl_persistent] shelves the [BiPlainly] premise, making proof
-search for the other premises fail. See the proof of [coreP_persistent] for an
-example where it would fail with a regular [Instance].*)
-Global Hint Extern 4 (Persistent _) =>
-  notypeclasses refine (impl_persistent _ _ _ _ _) : typeclass_instances.
diff --git a/tests/bi.ref b/tests/bi.ref
new file mode 100644
index 000000000..e69de29bb
diff --git a/tests/bi.v b/tests/bi.v
new file mode 100644
index 000000000..92f797609
--- /dev/null
+++ b/tests/bi.v
@@ -0,0 +1,9 @@
+From iris.bi Require Import bi plainly.
+
+(** See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/610 *)
+Lemma test_impl_persistent_1 `{!BiPlainly PROP} :
+  Persistent (PROP:=PROP) (True → True).
+Proof. apply _. Qed.
+Lemma test_impl_persistent_2 `{!BiPlainly PROP} :
+  Persistent (PROP:=PROP) (True → True → True).
+Proof. apply _. Qed.
-- 
GitLab