From e2e8748fe50292b720289a244779dd0519880824 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 11 Dec 2017 16:50:51 +0100
Subject: [PATCH] eta-expand bi_mor_exist and bi_mor_forall.

---
 theories/bi/derived_laws.v | 4 ++--
 theories/bi/interface.v    | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 996e434bf..dd997c89e 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -2306,12 +2306,12 @@ Section bi_morphims.
   Global Instance bi_mor_mono_flip : Proper (flip (⊢) ==> flip (⊢)) mor.
   Proof. solve_proper. Qed.
 
-  Lemma bi_mor_forall A Φ : mor (@bi_forall _ A Φ) ⊣⊢ (∀ x, mor (Φ x)).
+  Lemma bi_mor_forall A (Φ : A → PROP1) : mor (∀ x, Φ x) ⊣⊢ (∀ x, mor (Φ x)).
   Proof.
     apply bi.equiv_spec; split; [|apply bi_mor_forall_2].
     apply bi.forall_intro=>?. by rewrite bi.forall_elim.
   Qed.
-  Lemma bi_mor_exist A Φ : mor (@bi_exist _ A Φ) ⊣⊢ (∃ x, mor (Φ x)).
+  Lemma bi_mor_exist A (Φ : A → PROP1) : mor (∃ x, Φ x) ⊣⊢ (∃ x, mor (Φ x)).
   Proof.
     apply bi.equiv_spec; split; [apply bi_mor_exist_1|].
     apply bi.exist_elim=>?. by rewrite -bi.exist_intro.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 18bc2ad2a..e756e9058 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -342,8 +342,8 @@ Class BiMorphism {PROP1 PROP2 : bi} (f : PROP1 → PROP2) := {
   bi_mor_mono :> Proper ((⊢) ==> (⊢)) f;
   bi_mor_emp : f emp ⊣⊢ emp;
   bi_mor_impl_2 P Q : (f P → f Q)%I ⊢ f (P → Q)%I;
-  bi_mor_forall_2 A Φ : (∀ x, f (Φ x)) ⊢ f (@bi_forall _ A Φ);
-  bi_mor_exist_1 A Φ : f (@bi_exist _ A Φ) ⊢ ∃ x, f (Φ x);
+  bi_mor_forall_2 A (Φ : A → PROP1) : (∀ x, f (Φ x)) ⊢ f (∀ x, Φ x);
+  bi_mor_exist_1 A (Φ : A → PROP1) : f (∃ x, Φ x) ⊢ ∃ x, f (Φ x);
   bi_mor_internal_eq_1 (A : ofeT) (x y : A) : f (x ≡ y) ⊢ (x ≡ y);
   bi_mor_sep P Q : f (P ∗ Q) ⊣⊢ (f P ∗ f Q);
   bi_mor_wand_2 P Q : (f P -∗ f Q) ⊢ f (P -∗ Q);
-- 
GitLab