diff options
| author | Jasper Hugunin | 2020-09-09 12:48:07 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-09-16 12:46:57 -0700 |
| commit | d0aea47877be293f96e4662824c5d4728c8334b7 (patch) | |
| tree | 15fda556fbc5a6fb0e6252158ed9a3d7653b57ae | |
| parent | a75bf2d79391d5ab8b738da48e11db647bdec680 (diff) | |
Modify Arith/Mult.v to compile with -mangle-names
| -rw-r--r-- | theories/Arith/Mult.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |