From da93dcfaecc6475f2cda7109cf6f664db03ee351 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Fri, 9 Oct 2020 20:14:10 -0700
Subject: Modify ZArith/Znat.v to compile with -mangle-names

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