From d9ce5d4a8c3cd252a50529074455b07737679746 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Wed, 9 Sep 2020 12:53:52 -0700
Subject: Modify Arith/Between.v to compile with -mangle-names

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

diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 1db3f87cac..74d1e391c4 100644
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -110,7 +110,7 @@ Section Between.
   Lemma between_in_int :
     forall k l, between k l -> forall r, in_int k l r -> P r.
   Proof.
-    induction 1; intros.
+    intro k; induction 1 as [|l]; intros r ?.
     - absurd (k < k). { auto with arith. }
       eapply in_int_lt; eassumption.
     - destruct (in_int_p_Sq k l r) as [| ->]; auto with arith.
@@ -125,7 +125,7 @@ Section Between.
   Lemma exists_in_int :
     forall k l, exists_between k l -> exists2 m : nat, in_int k l m & Q m.
   Proof.
-    induction 1 as [* ? (p, ?, ?)|].
+    induction 1 as [* ? (p, ?, ?)|l].
     - exists p; auto with arith.
     - exists l; auto with arith.
   Qed.
@@ -154,7 +154,7 @@ Section Between.
       between k l ->
       (forall n:nat, in_int k l n -> P n -> ~ Q n) -> ~ exists_between k l.
   Proof.
-    induction 1; red; intros.
+    intro k; induction 1 as [|l]; red; intros.
     - absurd (k < k); auto with arith.
     - absurd (Q l). { auto with arith. }
       destruct (exists_in_int k (S l)) as (l',[],?).
-- 
cgit v1.2.3