diff options
| author | Jasper Hugunin | 2020-08-25 13:13:26 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-08-25 13:53:32 -0700 |
| commit | 1b6b14b1727a74a56727e38a1c58b1d93747135b (patch) | |
| tree | f82b0b09a4fbba864fd05cfa733e84fd13e026a3 /theories | |
| parent | 1a7dfd1bfce28a0ff20ba4ce58440d99bca3fbb3 (diff) | |
Modify Numbers/NatInt/NZAdd.v to compile with -mangle-names
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Numbers/NatInt/NZAdd.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v index 7982411bdd..66cbba9e08 100644 --- a/theories/Numbers/NatInt/NZAdd.v +++ b/theories/Numbers/NatInt/NZAdd.v @@ -22,7 +22,7 @@ Ltac nzsimpl' := autorewrite with nz nz'. Theorem add_0_r : forall n, n + 0 == n. Proof. - nzinduct n. + intro n; nzinduct n. - now nzsimpl. - intro. nzsimpl. now rewrite succ_inj_wd. Qed. |