From ceedda120493b46a6becdb48573d5295623d5066 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 13 Aug 2022 16:58:33 -0400
Subject: [PATCH] move MakePersistently instances to the correct file

---
 iris/proofmode/class_instances_frame.v | 11 -----------
 iris/proofmode/class_instances_make.v  | 14 ++++++++++++++
 2 files changed, 14 insertions(+), 11 deletions(-)

diff --git a/iris/proofmode/class_instances_frame.v b/iris/proofmode/class_instances_frame.v
index 26065b4ec..2c9d71237 100644
--- a/iris/proofmode/class_instances_frame.v
+++ b/iris/proofmode/class_instances_frame.v
@@ -177,17 +177,6 @@ Proof.
   rewrite /Frame /MakeAbsorbingly=> <- <- /=. by rewrite absorbingly_sep_r.
 Qed.
 
-Global Instance make_persistently_emp : @KnownMakePersistently PROP emp True.
-Proof.
-  by rewrite /KnownMakePersistently /MakePersistently
-     -persistently_True_emp persistently_pure.
-Qed.
-Global Instance make_persistently_True : @KnownMakePersistently PROP True True.
-Proof. by rewrite /KnownMakePersistently /MakePersistently persistently_pure. Qed.
-Global Instance make_persistently_default P :
-  MakePersistently P (<pers> P) | 100.
-Proof. by rewrite /MakePersistently. Qed.
-
 Global Instance frame_persistently R P Q Q' :
   Frame true R P Q → MakePersistently Q Q' →
   Frame true R (<pers> P) Q' | 2. (* Same cost as default. *)
diff --git a/iris/proofmode/class_instances_make.v b/iris/proofmode/class_instances_make.v
index 3fef78dbe..336873be2 100644
--- a/iris/proofmode/class_instances_make.v
+++ b/iris/proofmode/class_instances_make.v
@@ -117,6 +117,20 @@ Qed.
 Global Instance make_absorbingly_default P : MakeAbsorbingly P (<absorb> P) | 100.
 Proof. by rewrite /MakeAbsorbingly. Qed.
 
+(** Persistently *)
+Global Instance make_persistently_emp :
+  @KnownMakePersistently PROP emp True | 0.
+Proof.
+  by rewrite /KnownMakePersistently /MakePersistently
+     -persistently_True_emp persistently_pure.
+Qed.
+Global Instance make_persistently_True :
+  @KnownMakePersistently PROP True True | 0.
+Proof. by rewrite /KnownMakePersistently /MakePersistently persistently_pure. Qed.
+Global Instance make_persistently_default P :
+  MakePersistently P (<pers> P) | 100.
+Proof. by rewrite /MakePersistently. Qed.
+
 (** Intuitionistically *)
 Global Instance make_intuitionistically_emp :
   @KnownMakeIntuitionistically PROP emp emp | 0.
-- 
GitLab