diff options
| author | Jasper Hugunin | 2020-08-25 13:14:04 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-08-25 13:53:33 -0700 |
| commit | 9cd62a46c1db28e3bc77711ee6e7ab8e887ce494 (patch) | |
| tree | 50e13c709fce71c6b30b72dd0ca28d4848fbc59f | |
| parent | 1b6b14b1727a74a56727e38a1c58b1d93747135b (diff) | |
Modify Numbers/NatInt/NZMul.v to compile with -mangle-names
| -rw-r--r-- | theories/Numbers/NatInt/NZMul.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v index 9ddf7cb0eb..3d6465191d 100644 --- a/theories/Numbers/NatInt/NZMul.v +++ b/theories/Numbers/NatInt/NZMul.v @@ -17,7 +17,7 @@ Include NZAddProp NZ NZBase. Theorem mul_0_r : forall n, n * 0 == 0. Proof. -nzinduct n; intros; now nzsimpl. +intro n; nzinduct n; intros; now nzsimpl. Qed. Theorem mul_succ_r : forall n m, n * (S m) == n * m + n. |