From d0aea47877be293f96e4662824c5d4728c8334b7 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Wed, 9 Sep 2020 12:48:07 -0700
Subject: Modify Arith/Mult.v to compile with -mangle-names

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

diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 507d956e81..d7f703e6e4 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -158,7 +158,7 @@ Fixpoint mult_acc (s:nat) m n : nat :=
 
 Lemma mult_acc_aux : forall n m p, m + n * p = mult_acc m p n.
 Proof.
-  induction n as [| n IHn]; simpl; auto.
+  intro n; induction n as [| n IHn]; simpl; auto.
   intros. rewrite Nat.add_assoc, IHn. f_equal.
   rewrite Nat.add_comm. apply plus_tail_plus.
 Qed.
-- 
cgit v1.2.3