From d997bf036afaac2778458c74156267d9bda06165 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 11 Jan 2018 11:23:17 -0800
Subject: [PATCH] FromAssumption instances.

---
 theories/proofmode/monpred.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 8b2c7657d..4f112a12e 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -86,6 +86,13 @@ Proof.
   apply  bi.affinely_persistently_if_elim.
 Qed.
 
+Global Instance from_assumption_make_monPred_all P Q :
+  FromAssumption p P Q → FromAssumption p (monPred_all P) Q.
+Proof. intros ?. by rewrite /FromAssumption monPred_all_elim. Qed.
+Global Instance from_assumption_make_monPred_ex P Q :
+  FromAssumption p P Q → FromAssumption p P (monPred_ex Q).
+Proof. intros ?. by rewrite /FromAssumption -monPred_ex_intro. Qed.
+
 Global Instance as_valid_monPred_at φ P (Φ : I → PROP) :
   AsValid φ P → (∀ i, MakeMonPredAt i P (Φ i)) → AsValid' φ (∀ i, Φ i) | 100.
 Proof.
-- 
GitLab