From a75bf2d79391d5ab8b738da48e11db647bdec680 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Wed, 9 Sep 2020 12:46:49 -0700
Subject: Modify Arith/Plus.v to compile with -mangle-names

---
 theories/Arith/Plus.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index ec7426e648..5da7738adc 100644
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -156,7 +156,7 @@ Fixpoint tail_plus n m : nat :=
 
 Lemma plus_tail_plus : forall n m, n + m = tail_plus n m.
 Proof.
-induction n as [| n IHn]; simpl; auto.
+intro n; induction n as [| n IHn]; simpl; auto.
 intro m; rewrite <- IHn; simpl; auto.
 Qed.
 
-- 
cgit v1.2.3