From ad06e03a72f6823c962356e6c65f06c0cab6599e Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 14 Dec 2017 17:55:06 +0100
Subject: [PATCH] Fix type of monPred_bi_embedding and monPred_sbi_embedding.

---
 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 7caa5644c..740e7aa85 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -469,7 +469,7 @@ Proof.
 Qed.
 
 Global Instance monPred_bi_embedding :
-  Inhabited I → @BiEmbedding PROP (monPredI I PROP) bi_embed.
+  Inhabited I → BiEmbedding PROP (monPredI I PROP).
 Proof.
   split; try apply _; unseal; try done.
   - move =>?? /= [/(_ inhabitant) ?] //.
@@ -502,6 +502,6 @@ Proof.
 Qed.
 
 Global Instance monPred_sbi_embedding :
-  Inhabited I → @SbiEmbedding PROP (monPredSI I PROP) bi_embed.
+  Inhabited I → SbiEmbedding PROP (monPredSI I PROP).
 Proof. split; try apply _. by unseal. Qed.
 End sbi_facts.
-- 
GitLab