From 9daa2ec464eb9b881cab7d53fd39efc5de3afe12 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Sat, 12 Sep 2020 18:01:56 -0700
Subject: Modify NArith/Nnat.v to compile with -mangle-names

---
 theories/NArith/Nnat.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v
index 43fa8516d3..48df5fe884 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.v
@@ -70,7 +70,7 @@ Lemma inj_sub a a' :
   N.to_nat (a - a') = N.to_nat a - N.to_nat a'.
 Proof.
  destruct a as [|a], a' as [|a']; simpl; rewrite ?Nat.sub_0_r; trivial.
- destruct (Pos.compare_spec a a').
+ destruct (Pos.compare_spec a a') as [H|H|H].
  - subst. now rewrite Pos.sub_mask_diag, Nat.sub_diag.
  - rewrite Pos.sub_mask_neg; trivial. apply Pos2Nat.inj_lt in H.
    simpl; symmetry; apply Nat.sub_0_le. now apply Nat.lt_le_incl.
@@ -93,8 +93,8 @@ Qed.
 Lemma inj_compare a a' :
  (a ?= a')%N = (N.to_nat a ?= N.to_nat a').
 Proof.
- destruct a, a'; simpl; trivial.
- - now destruct (Pos2Nat.is_succ p) as (n,->).
+ destruct a as [|p], a' as [|p']; simpl; trivial.
+ - now destruct (Pos2Nat.is_succ p') as (n,->).
  - now destruct (Pos2Nat.is_succ p) as (n,->).
  - apply Pos2Nat.inj_compare.
 Qed.
-- 
cgit v1.2.3