diff options
| author | Jasper Hugunin | 2020-10-09 20:14:10 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-10-11 19:05:14 -0700 |
| commit | da93dcfaecc6475f2cda7109cf6f664db03ee351 (patch) | |
| tree | 941410d05f221d473f67d29f5813db56fc5bb9e1 /theories/ZArith | |
| parent | 8788d6d1d39e30cc54b8652301c70fe759238894 (diff) | |
Modify ZArith/Znat.v to compile with -mangle-names
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/Znat.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index 6a82645ba6..7f72d42d1f 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -50,7 +50,7 @@ Qed. Lemma N_nat_Z n : Z.of_nat (N.to_nat n) = Z.of_N n. Proof. - destruct n; trivial. simpl. + destruct n as [|p]; trivial. simpl. destruct (Pos2Nat.is_succ p) as (m,H). rewrite H. simpl. f_equal. now apply SuccNat2Pos.inv. Qed. @@ -668,7 +668,7 @@ Qed. Lemma inj_abs_nat z : Z.of_nat (Z.abs_nat z) = Z.abs z. Proof. - destruct z; simpl; trivial; + destruct z as [|p|p]; simpl; trivial; destruct (Pos2Nat.is_succ p) as (n,H); rewrite H; simpl; f_equal; now apply SuccNat2Pos.inv. Qed. |