From 0991de1cc62d3ab0c5d8839810e92d78c5734bc8 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Wed, 9 Sep 2020 12:45:13 -0700
Subject: Modify Arith/Le.v to compile with -mangle-names

---
 theories/Arith/Le.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index 4f17a7a8d3..4e71465452 100644
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -80,7 +80,7 @@ Lemma le_elim_rel :
    (forall p (q:nat), p <= q -> P p q -> P (S p) (S q)) ->
    forall n m, n <= m -> P n m.
 Proof.
-  intros P H0 HS.
+  intros P H0 HS n.
   induction n; trivial.
   intros m Le. elim Le; auto with arith.
  Qed.
-- 
cgit v1.2.3