From 46ffdc4ad4d883fbc7cbd71c7be6769192754a95 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 18 Dec 2017 19:33:35 +0100
Subject: [PATCH] Name some variables.
---
theories/bi/embedding.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index c34324351..ca132298d 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -45,7 +45,7 @@ Section bi_embedding.
Proof. solve_proper. Qed.
Global Instance bi_embed_inj : Inj (≡) (≡) bi_embed.
Proof.
- intros ?? EQ. apply bi.equiv_spec, conj; apply (inj bi_embed);
+ intros P Q EQ. apply bi.equiv_spec, conj; apply (inj bi_embed);
rewrite EQ //.
Qed.
--
GitLab