From 1a0017b8b85d2536d333f6b85f311aefa219b33a Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Sat, 12 Sep 2020 17:11:36 -0700
Subject: Modify Arith/Compare_dec.v to compile with -mangle-names

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

diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 341dd7de5d..1afc49b7ff 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -21,7 +21,7 @@ Defined.
 
 Definition lt_eq_lt_dec n m : {n < m} + {n = m} + {m < n}.
 Proof.
-  induction n in m |- *; destruct m; auto with arith.
+  induction n as [|n IHn] in m |- *; destruct m as [|m]; auto with arith.
   destruct (IHn m) as [H|H]; auto with arith.
   destruct H; auto with arith.
 Defined.
@@ -33,9 +33,9 @@ Defined.
 
 Definition le_lt_dec n m : {n <= m} + {m < n}.
 Proof.
-  induction n in m |- *.
+  induction n as [|n IHn] in m |- *.
   - left; auto with arith.
-  - destruct m.
+  - destruct m as [|m].
     + right; auto with arith.
     + elim (IHn m); [left|right]; auto with arith.
 Defined.
-- 
cgit v1.2.3