From f136bcf5a067fcf1e38f48062ccde06875709e6a Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Fri, 9 Oct 2020 15:49:42 -0700
Subject: Modify setoid_ring/Ring.v to compile with -mangle-names

---
 theories/setoid_ring/Ring.v | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/theories/setoid_ring/Ring.v b/theories/setoid_ring/Ring.v
index a66037a956..25b79d1fb2 100644
--- a/theories/setoid_ring/Ring.v
+++ b/theories/setoid_ring/Ring.v
@@ -17,22 +17,22 @@ Require Export Ring_tac.
 Lemma BoolTheory :
   ring_theory false true xorb andb xorb (fun b:bool => b) (eq(A:=bool)).
 split; simpl.
-destruct x; reflexivity.
-destruct x; destruct y; reflexivity.
-destruct x; destruct y; destruct z; reflexivity.
+intros x; destruct x; reflexivity.
+intros x y; destruct x; destruct y; reflexivity.
+intros x y z; destruct x; destruct y; destruct z; reflexivity.
 reflexivity.
-destruct x; destruct y; reflexivity.
-destruct x; destruct y; reflexivity.
-destruct x; destruct y; destruct z; reflexivity.
+intros x y; destruct x; destruct y; reflexivity.
+intros x y; destruct x; destruct y; reflexivity.
+intros x y z; destruct x; destruct y; destruct z; reflexivity.
 reflexivity.
-destruct x; reflexivity.
+intros x; destruct x; reflexivity.
 Qed.
 
 Definition bool_eq (b1 b2:bool) :=
   if b1 then b2 else negb b2.
 
 Lemma bool_eq_ok : forall b1 b2, bool_eq b1 b2 = true -> b1 = b2.
-destruct b1; destruct b2; auto.
+intros b1 b2; destruct b1; destruct b2; auto.
 Qed.
 
 Ltac bool_cst t :=
-- 
cgit v1.2.3