From 1a7dfd1bfce28a0ff20ba4ce58440d99bca3fbb3 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Tue, 25 Aug 2020 13:11:43 -0700
Subject: Modify Numbers/NatInt/NZBase.v to compile with -mangle-names

---
 theories/Numbers/NatInt/NZBase.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 8bc393bbad..e6eabd5b2c 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -74,7 +74,7 @@ Proof.
 intros z Base Step; revert Base; pattern z; apply bi_induction.
 - solve_proper.
 - intro; now apply bi_induction.
-- intro; pose proof (Step n); tauto.
+- intro n; pose proof (Step n); tauto.
 Qed.
 
 End CentralInduction.
-- 
cgit v1.2.3