From 79bddd1a21530235b73e551e77febd372e46201d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 3 Nov 2017 01:15:27 +0100
Subject: [PATCH] `IntoForall` and `FromForall` instances for `except_0`.

---
 theories/proofmode/class_instances.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 3f5dedbc6..9f5d718b0 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -772,6 +772,9 @@ Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.
 Global Instance into_forall_later {A} P (Φ : A → uPred M) :
   IntoForall P Φ → IntoForall (▷ P) (λ a, ▷ (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP later_forall. Qed.
+Global Instance into_forall_except_0 {A} P (Φ : A → uPred M) :
+  IntoForall P Φ → IntoForall (◇ P) (λ a, ◇ (Φ a))%I.
+Proof. rewrite /IntoForall=> HP. by rewrite HP except_0_forall. Qed.
 
 (* FromForall *)
 Global Instance from_forall_forall {A} (Φ : A → uPred M) :
@@ -801,6 +804,9 @@ Proof. rewrite /FromForall=> <-. by rewrite persistently_forall. Qed.
 Global Instance from_forall_later {A} P (Φ : A → uPred M) :
   FromForall P Φ → FromForall (▷ P) (λ a, ▷ (Φ a))%I.
 Proof. rewrite /FromForall=> <-. by rewrite later_forall. Qed.
+Global Instance from_forall_except_0 {A} P (Φ : A → uPred M) :
+  FromForall P Φ → FromForall (◇ P) (λ a, ◇ (Φ a))%I.
+Proof. rewrite /FromForall=> <-. by rewrite except_0_forall. Qed.
 
 (* FromModal *)
 Global Instance from_modal_later P : FromModal (â–· P) P.
-- 
GitLab