From fc9ee09a175a8acd17c257b361bf1a4a3d05401c Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 11 Jan 2018 11:10:47 -0800
Subject: [PATCH] Minimal proof mode support for monPred_ex

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

diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 10948e7ce..8b2c7657d 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -267,6 +267,17 @@ Proof.
   rewrite /IntoForall /MakeMonPredAt=>H. setoid_rewrite <- H. by unseal.
 Qed.
 
+Global Instance from_exist_monPred_at_ex P (Φ : I → PROP) i :
+  (∀ i, MakeMonPredAt i P (Φ i)) → FromExist (monPred_ex P i) Φ.
+Proof.
+  rewrite /FromExist /MakeMonPredAt=>H. setoid_rewrite <- H. by unseal.
+Qed.
+Global Instance into_exist_monPred_at_ex P (Φ : I → PROP) i :
+  (∀ i, MakeMonPredAt i P (Φ i)) → IntoExist (monPred_ex P i) Φ.
+Proof.
+  rewrite /IntoExist /MakeMonPredAt=>H. setoid_rewrite <- H. by unseal.
+Qed.
+
 Global Instance from_forall_monPred_at {A} P (Φ : A → monPred) (Ψ : A → PROP) i :
   FromForall P Φ → (∀ a, MakeMonPredAt i (Φ a) (Ψ a)) → FromForall (P i) Ψ.
 Proof.
-- 
GitLab