diff options
| author | Jasper Hugunin | 2020-09-09 10:23:51 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-09-16 12:46:57 -0700 |
| commit | ecb29318d6b818b758ecf6d4a06dbde8838e7a04 (patch) | |
| tree | d0695129b20f21d2d1c4b00149fa9a6c7db5e45a | |
| parent | c66266493b3678814604365386e4b7afc362483c (diff) | |
Modify Numbers/Natural/Abstract/NAdd.v to compile with -mangle-names
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NAdd.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v index 8c4d072114..55c4b193a5 100644 --- a/theories/Numbers/Natural/Abstract/NAdd.v +++ b/theories/Numbers/Natural/Abstract/NAdd.v @@ -58,7 +58,7 @@ Qed. Theorem succ_add_discr : forall n m, m ~= S (n + m). Proof. -intro n; induct m. +intros n m; induct m. apply neq_sym. apply neq_succ_0. intros m IH H. apply succ_inj in H. rewrite add_succ_r in H. unfold not in IH; now apply IH. |