From e5880b643bb9ce6974d3ecffd8edcbfad9f45cd4 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Tue, 25 Aug 2020 13:02:59 -0700
Subject: Modify Relations/Relations.v to compile with -mangle-names

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

diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v
index 0a5128f093..dea76694f3 100644
--- a/theories/Relations/Relations.v
+++ b/theories/Relations/Relations.v
@@ -16,16 +16,16 @@ Lemma inverse_image_of_equivalence :
   forall (A B:Type) (f:A -> B) (r:relation B),
     equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)).
 Proof.
-  intros; split; elim H; red; auto.
+  intros A B f r H; split; elim H; red; auto.
   intros _ equiv_trans _ x y z H0 H1; apply equiv_trans with (f y); assumption.
 Qed.
 
 Lemma inverse_image_of_eq :
   forall (A B:Type) (f:A -> B), equivalence A (fun x y:A => f x = f y).
 Proof.
-  split; red;
+  intros A B f; split; red;
     [  (* reflexivity *) reflexivity
-      |  (* transitivity *) intros; transitivity (f y); assumption
+      |  (* transitivity *) intros x y z; transitivity (f y); assumption
       |  (* symmetry *) intros; symmetry ; assumption ].
 Qed.
 
-- 
cgit v1.2.3