From ef7dbd83b583abf08f162e343250507ad74744a1 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Tue, 15 Dec 2020 21:00:29 -0800
Subject: Modify Logic/JMeq.v to compile with -mangle-names

---
 theories/Logic/JMeq.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 7ee3a99d60..21eed3a696 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -39,8 +39,8 @@ Definition JMeq_hom {A : Type} (x y : A) := JMeq x y.
 Register JMeq_hom as core.JMeq.hom.
 
 Lemma JMeq_sym : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x.
-Proof. 
-intros; destruct H; trivial.
+Proof.
+intros A B x y H; destruct H; trivial.
 Qed.
 
 #[global]
@@ -150,7 +150,7 @@ Lemma JMeq_eq_dep :
   forall U (P:U->Type) p q (x:P p) (y:P q), 
   p = q -> JMeq x y -> eq_dep U P p x q y.
 Proof.
-intros.
+intros U P p q x y H H0.
 destruct H.
 apply JMeq_eq in H0 as ->.
 reflexivity.
-- 
cgit v1.2.3