From bce1a24ca7e9a9e71047fd145668ec2fbe0fd2ef Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 1 Mar 2018 15:42:24 +0100
Subject: [PATCH] Turn some MaybeLaterN instances into LaterN instances.

---
 theories/proofmode/class_instances.v | 24 ++++++++++--------------
 theories/proofmode/monpred.v         |  6 +++---
 2 files changed, 13 insertions(+), 17 deletions(-)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index b638109f4..730dea755 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -1609,24 +1609,20 @@ Proof.
 Qed.
 
 Global Instance into_later_affinely n P Q :
-  MaybeIntoLaterN false n P Q →
-  MaybeIntoLaterN false n (bi_affinely P) (bi_affinely Q).
-Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite laterN_affinely_2. Qed.
+  IntoLaterN false n P Q → IntoLaterN false n (bi_affinely P) (bi_affinely Q).
+Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_affinely_2. Qed.
 Global Instance into_later_absorbingly n P Q :
-  MaybeIntoLaterN false n P Q →
-  MaybeIntoLaterN false n (bi_absorbingly P) (bi_absorbingly Q).
-Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite laterN_absorbingly. Qed.
+  IntoLaterN false n P Q → IntoLaterN false n (bi_absorbingly P) (bi_absorbingly Q).
+Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_absorbingly. Qed.
 Global Instance into_later_plainly n P Q :
-  MaybeIntoLaterN false n P Q →
-  MaybeIntoLaterN false n (bi_plainly P) (bi_plainly Q).
-Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite laterN_plainly. Qed.
+  IntoLaterN false n P Q → IntoLaterN false n (bi_plainly P) (bi_plainly Q).
+Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_plainly. Qed.
 Global Instance into_later_persistently n P Q :
-  MaybeIntoLaterN false n P Q →
-  MaybeIntoLaterN false n (bi_persistently P) (bi_persistently Q).
-Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite laterN_persistently. Qed.
+  IntoLaterN false n P Q → IntoLaterN false n (bi_persistently P) (bi_persistently Q).
+Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_persistently. Qed.
 Global Instance into_later_embed`{SbiEmbedding PROP PROP'} n P Q :
-  MaybeIntoLaterN false n P Q → MaybeIntoLaterN false n ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite sbi_embed_laterN. Qed.
+  IntoLaterN false n P Q → IntoLaterN false n ⎡P⎤ ⎡Q⎤.
+Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite sbi_embed_laterN. Qed.
 
 Global Instance into_laterN_sep_l n P1 P2 Q1 Q2 :
   IntoLaterN false n P1 Q1 → MaybeIntoLaterN false n P2 Q2 →
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index cfec41ed6..b5a92ce01 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -426,10 +426,10 @@ Global Instance into_except_0_monPred_at_bwd i P 𝓟 Q :
 Proof. rewrite /IntoExcept0 /MakeMonPredAt=> H <-. by rewrite H monPred_at_except_0. Qed.
 
 Global Instance maybe_into_later_monPred_at i n P Q 𝓠 :
-  MaybeIntoLaterN false n P Q → MakeMonPredAt i Q 𝓠 →
-  MaybeIntoLaterN false n (P i) 𝓠.
+  IntoLaterN false n P Q → MakeMonPredAt i Q 𝓠 →
+  IntoLaterN false n (P i) 𝓠.
 Proof.
-  rewrite /MaybeIntoLaterN /MakeMonPredAt=> -> <-. elim n=>//= ? <-.
+  rewrite /IntoLaterN /MaybeIntoLaterN /MakeMonPredAt=> -> <-. elim n=>//= ? <-.
    by rewrite monPred_at_later.
 Qed.
 Global Instance from_later_monPred_at i n P Q 𝓠 :
-- 
GitLab