From af7b79f52f0f9d900142930114b02a34b9091a78 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Fri, 9 Oct 2020 20:15:07 -0700
Subject: Modify ZArith/Zabs.v to compile with -mangle-names

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

diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index 21086d9b61..f869e15023 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -49,12 +49,12 @@ Qed.
 
 Theorem Zabs_intro : forall P (n:Z), P (- n) -> P n -> P (Z.abs n).
 Proof.
- now destruct n.
+ intros P n; now destruct n.
 Qed.
 
 Definition Zabs_dec : forall x:Z, {x = Z.abs x} + {x = - Z.abs x}.
 Proof.
- destruct x; auto.
+ intros x; destruct x; auto.
 Defined.
 
 Lemma Zabs_spec x :
-- 
cgit v1.2.3