From 2b06f3e29f48541505b13fcb65ede25ab3d4627b Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 5 Mar 2018 18:45:31 +0100
Subject: [PATCH] Make sure as_valid_embed is not used when there is no
 embedding.

---
 theories/proofmode/class_instances.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index e36469146..d6d8907ff 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -1007,9 +1007,16 @@ Proof.
   - intros x. apply H1. revert H2. by rewrite (bi.forall_elim x).
 Qed.
 
+(* We add a useless hypothesis [BiEmbed PROP PROP'] in order to make
+   sure this iinstance is not used when there is no embedding between
+   PROP and PROP'.
+   The first [`{BiEmbed PROP PROP'}] is not considered as a premise by
+   Coq TC search mechanism because the rest of the hypothesis is dependent
+   on it. *)
 Global Instance as_valid_embed `{BiEmbed PROP PROP'} (φ : Prop) (P : PROP) :
+  BiEmbed PROP PROP' →
   AsValid0 φ P → AsValid φ ⎡P⎤.
-Proof. rewrite /AsValid0 /AsValid=> ->. rewrite embed_valid //. Qed.
+Proof. rewrite /AsValid0 /AsValid=> _ ->. rewrite embed_valid //. Qed.
 End bi_instances.
 
 Section sbi_instances.
-- 
GitLab