From 6c0eb97a2e0dc92d1af18ea37279af4f8f2378a8 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 6 Feb 2018 20:59:15 +0100
Subject: [PATCH] Fix Absolute instances.

---
 theories/bi/monpred.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index aa2e54c84..b20c1206d 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -635,7 +635,7 @@ Global Instance plainly_absolute P : Absolute (bi_plainly P).
 Proof. apply emb_absolute. Qed.
 Global Instance absolutely_absolute P : Absolute (∀ᵢ P).
 Proof. apply emb_absolute. Qed.
-Global Instance monPred_relatively_absolute P : Absolute (∃ᵢ P).
+Global Instance relatively_absolute P : Absolute (∃ᵢ P).
 Proof. apply emb_absolute. Qed.
 
 Global Instance and_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P ∧ Q).
@@ -653,7 +653,7 @@ Global Instance forall_absolute {A} Φ {H : ∀ x : A, Absolute (Φ x)} :
   @Absolute I PROP (∀ x, Φ x)%I.
 Proof. intros ??. unseal. do 2 f_equiv. by apply absolute_at. Qed.
 Global Instance exists_absolute {A} Φ {H : ∀ x : A, Absolute (Φ x)} :
-  @Absolute I PROP (∀ x, Φ x)%I.
+  @Absolute I PROP (∃ x, Φ x)%I.
 Proof. intros ??. unseal. do 2 f_equiv. by apply absolute_at. Qed.
 
 Global Instance sep_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P ∗ Q).
-- 
GitLab