From ecb29318d6b818b758ecf6d4a06dbde8838e7a04 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Wed, 9 Sep 2020 10:23:51 -0700
Subject: Modify Numbers/Natural/Abstract/NAdd.v to compile with -mangle-names

---
 theories/Numbers/Natural/Abstract/NAdd.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v
index 8c4d072114..55c4b193a5 100644
--- a/theories/Numbers/Natural/Abstract/NAdd.v
+++ b/theories/Numbers/Natural/Abstract/NAdd.v
@@ -58,7 +58,7 @@ Qed.
 
 Theorem succ_add_discr : forall n m, m ~= S (n + m).
 Proof.
-intro n; induct m.
+intros n m; induct m.
 apply neq_sym. apply neq_succ_0.
 intros m IH H. apply succ_inj in H. rewrite add_succ_r in H.
 unfold not in IH; now apply IH.
-- 
cgit v1.2.3