From 0f6f3eedb65c3b061b4d4443c18e57ad38bb1f41 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Sat, 12 Sep 2020 17:09:44 -0700
Subject: Modify Arith/Peano_dec.v to compile with -mangle-names

---
 theories/Arith/Peano_dec.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index a673a1119f..9a7a397023 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -16,7 +16,7 @@ Implicit Types m n x y : nat.
 
 Theorem O_or_S n : {m : nat | S m = n} + {0 = n}.
 Proof.
-  induction n.
+  induction n as [|n IHn].
   - now right.
   - left; exists n; auto.
 Defined.
@@ -47,7 +47,7 @@ pose (def_n2 := eq_refl n0); transitivity (eq_ind _ _ le_mn2 _ def_n2).
   2: reflexivity.
 generalize def_n2; revert le_mn1 le_mn2.
 generalize n0 at 1 4 5 7; intros n1 le_mn1.
-destruct le_mn1; intros le_mn2; destruct le_mn2.
+destruct le_mn1 as [|? le_mn1]; intros le_mn2; destruct le_mn2 as [|? le_mn2].
 + now intros def_n0; rewrite (UIP_nat _ _ def_n0 eq_refl).
 + intros def_n0; generalize le_mn2; rewrite <-def_n0; intros le_mn0.
   now destruct (Nat.nle_succ_diag_l _ le_mn0).
-- 
cgit v1.2.3