From d5c202a71004f8f4b2ef7f0f8fc398a8ebcf8065 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Thu, 8 Oct 2020 18:40:52 -0700
Subject: Modify ZArith/Zorder.v to compile with -mangle-names

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

diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 7e33fe2b4c..949a01860f 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -354,7 +354,7 @@ Qed.
 
 Lemma Zle_0_nat : forall n:nat, 0 <= Z.of_nat n.
 Proof.
-  induction n; simpl; intros. apply Z.le_refl. easy.
+  intros n; induction n; simpl; intros. apply Z.le_refl. easy.
 Qed.
 
 Hint Immediate Z.eq_le_incl: zarith.
-- 
cgit v1.2.3