From e2850002db0271aff914c6a81d17354991b0d5cb Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Fri, 8 Jan 2021 14:00:50 -0800
Subject: Modify Classes/SetoidClass.v to compile with -mangle-names

---
 theories/Classes/SetoidClass.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 6a98af39aa..3e71a60fa6 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -87,7 +87,7 @@ Tactic Notation "clsubst" "*" := clsubst_nofail.
 
 Lemma nequiv_equiv_trans : forall `{Setoid A} (x y z : A), x =/= y -> y == z -> x =/= z.
 Proof with auto.
-  intros; intro.
+  intros A ? x y z H H0 H1.
   assert(z == y) by (symmetry ; auto).
   assert(x == y) by (transitivity z ; eauto).
   contradiction.
@@ -95,7 +95,7 @@ Qed.
 
 Lemma equiv_nequiv_trans : forall `{Setoid A} (x y z : A), x == y -> y =/= z -> x =/= z.
 Proof.
-  intros; intro.
+  intros A ? x y z **; intro.
   assert(y == x) by (symmetry ; auto).
   assert(y == z) by (transitivity x ; eauto).
   contradiction.
-- 
cgit v1.2.3