From e772028ac714f93b8155f839193a9ccde5487084 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 11 Mar 2017 10:35:08 +0100
Subject: [PATCH] Fix issue #74.

---
 theories/proofmode/class_instances.v | 22 ++++++++--------------
 theories/tests/proofmode.v           |  8 ++++++++
 2 files changed, 16 insertions(+), 14 deletions(-)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index cb627c7c7..e5542fcab 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -135,12 +135,6 @@ Global Instance into_persistentP_persistent P :
 Proof. done. Qed.
 
 (* IntoLater *)
-Global Instance into_laterN_default n P : IntoLaterN n P P | 1000.
-Proof. apply laterN_intro. Qed.
-Global Instance into_laterN_progress P Q :
-  IntoLaterN' n P Q → IntoLaterN n P Q.
-Proof. done. Qed.
-
 Global Instance into_laterN_later n P Q :
   IntoLaterN n P Q → IntoLaterN' (S n) (▷ P) Q.
 Proof. by rewrite /IntoLaterN' /IntoLaterN =>->. Qed.
@@ -152,32 +146,32 @@ Proof. rewrite /IntoLaterN' /IntoLaterN=>->. by rewrite laterN_plus. Qed.
 
 Global Instance into_laterN_and_l n P1 P2 Q1 Q2 :
   IntoLaterN' n P1 Q1 → IntoLaterN n P2 Q2 →
-  IntoLaterN n (P1 ∧ P2) (Q1 ∧ Q2).
+  IntoLaterN' n (P1 ∧ P2) (Q1 ∧ Q2) | 10.
 Proof. rewrite /IntoLaterN' /IntoLaterN=> -> ->. by rewrite laterN_and. Qed.
 Global Instance into_laterN_and_r n P P2 Q2 :
-  IntoLaterN' n P2 Q2 → IntoLaterN' n (P ∧ P2) (P ∧ Q2).
+  IntoLaterN' n P2 Q2 → IntoLaterN' n (P ∧ P2) (P ∧ Q2) | 11.
 Proof.
   rewrite /IntoLaterN' /IntoLaterN=> ->. by rewrite laterN_and -(laterN_intro _ P).
-  Qed.
+Qed.
 
 Global Instance into_laterN_or_l n P1 P2 Q1 Q2 :
   IntoLaterN' n P1 Q1 → IntoLaterN n P2 Q2 →
-  IntoLaterN n (P1 ∨ P2) (Q1 ∨ Q2).
+  IntoLaterN' n (P1 ∨ P2) (Q1 ∨ Q2) | 10.
 Proof. rewrite /IntoLaterN' /IntoLaterN=> -> ->. by rewrite laterN_or. Qed.
 Global Instance into_laterN_or_r n P P2 Q2 :
   IntoLaterN' n P2 Q2 →
-  IntoLaterN' n (P ∨ P2) (P ∨ Q2).
+  IntoLaterN' n (P ∨ P2) (P ∨ Q2) | 11.
 Proof.
   rewrite /IntoLaterN' /IntoLaterN=> ->. by rewrite laterN_or -(laterN_intro _ P).
 Qed.
 
 Global Instance into_laterN_sep_l n P1 P2 Q1 Q2 :
   IntoLaterN' n P1 Q1 → IntoLaterN n P2 Q2 →
-  IntoLaterN n (P1 ∗ P2) (Q1 ∗ Q2).
-Proof. intros ??; red. by rewrite laterN_sep; apply sep_mono. Qed.
+  IntoLaterN' n (P1 ∗ P2) (Q1 ∗ Q2) | 10.
+Proof. rewrite /IntoLaterN' /IntoLaterN=> -> ->. by rewrite laterN_sep. Qed.
 Global Instance into_laterN_sep_r n P P2 Q2 :
   IntoLaterN' n P2 Q2 →
-  IntoLaterN' n (P ∗ P2) (P ∗ Q2).
+  IntoLaterN' n (P ∗ P2) (P ∗ Q2) | 11.
 Proof.
   rewrite /IntoLaterN' /IntoLaterN=> ->. by rewrite laterN_sep -(laterN_intro _ P).
 Qed.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index b32d5780a..a5eb0623d 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -153,3 +153,11 @@ Proof.
   iIntros "HP". iAssert (▷ _ -∗ ▷ P)%I as "?"; last done.
   iIntros "?". iNext. iAssumption.
 Qed.
+
+Lemma test_iNext_sep (M : ucmraT) (P Q : uPred M)
+    (R1 := (P ∗ Q)%I) (R2 := (▷ P ∗ ▷ Q)%I) :
+  (▷ P ∗ ▷ Q) ∗ R1 ∗ R2 -∗ ▷ (P ∗ Q) ∗ ▷ R1 ∗ R2.
+Proof.
+  iIntros "H". iNext.
+  rewrite {1 2}(lock R1). (* check whether R1 has not been unfolded *) done.
+Qed.
-- 
GitLab