From 2b69114de48693391de1240784d55d8d9b73cb1c Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Fri, 9 Oct 2020 20:19:03 -0700
Subject: Modify ZArith/Zpow_def.v to compile with -mangle-names

---
 theories/ZArith/Zpow_def.v | 6 +++---
 1 file 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.
-- 
cgit v1.2.3