From f8449f4efcc6cee1555cadf09a8828cf176556ac Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Wed, 9 Sep 2020 10:28:13 -0700
Subject: Modify Numbers/Natural/Abstract/NAddOrder.v to compile with
 -mangle-names

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

diff --git a/theories/Numbers/Natural/Abstract/NAddOrder.v b/theories/Numbers/Natural/Abstract/NAddOrder.v
index 7c74de6364..d0ef94d1a4 100644
--- a/theories/Numbers/Natural/Abstract/NAddOrder.v
+++ b/theories/Numbers/Natural/Abstract/NAddOrder.v
@@ -19,7 +19,7 @@ Include NOrderProp N.
 
 Theorem le_add_r : forall n m, n <= n + m.
 Proof.
-intro n; induct m.
+intros n m; induct m.
 rewrite add_0_r; now apply eq_le_incl.
 intros m IH. rewrite add_succ_r; now apply le_le_succ_r.
 Qed.
-- 
cgit v1.2.3