diff options
| author | Jasper Hugunin | 2020-10-09 20:19:03 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-10-11 19:05:14 -0700 |
| commit | 2b69114de48693391de1240784d55d8d9b73cb1c (patch) | |
| tree | c3b326b34c6c92476ba3ce7b29df8227376db35b /theories/ZArith | |
| parent | c513ab654b2de5a80a5bc71b9a0769c46e5b55cd (diff) | |
Modify ZArith/Zpow_def.v to compile with -mangle-names
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/Zpow_def.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/ZArith/Zpow_def.v b/theories/ZArith/Zpow_def.v index 8609a6af98..d4f58c3b04 100644 --- a/theories/ZArith/Zpow_def.v +++ b/theories/ZArith/Zpow_def.v @@ -25,9 +25,9 @@ Notation Zpower_Ppow := Pos2Z.inj_pow (only parsing). Lemma Zpower_theory : power_theory 1 Z.mul (@eq Z) Z.of_N Z.pow. Proof. - constructor. intros. - destruct n;simpl;trivial. + constructor. intros z n. + destruct n as [|p];simpl;trivial. unfold Z.pow_pos. rewrite <- (Z.mul_1_r (pow_pos _ _ _)). generalize 1. - induction p; simpl; intros; rewrite ?IHp, ?Z.mul_assoc; trivial. + induction p as [p IHp|p IHp|]; simpl; intros; rewrite ?IHp, ?Z.mul_assoc; trivial. Qed. |