From 32ce4406474bca0b3fa21834fec978786802a907 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Fri, 9 Oct 2020 20:20:03 -0700
Subject: Modify micromega/ZCoeff.v to compile with -mangle-names

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

diff --git a/theories/micromega/ZCoeff.v b/theories/micromega/ZCoeff.v
index 4e04adaddb..aaaeb9e118 100644
--- a/theories/micromega/ZCoeff.v
+++ b/theories/micromega/ZCoeff.v
@@ -121,7 +121,7 @@ Qed.
 
 Lemma phi_pos1_pos : forall x : positive, 0 < phi_pos1 x.
 Proof.
-induction x as [x IH | x IH |]; simpl;
+intros x; induction x as [x IH | x IH |]; simpl;
 try apply (Rplus_pos_pos sor); try apply (Rtimes_pos_pos sor); try apply (Rplus_pos_pos sor);
 try apply (Rlt_0_1 sor); assumption.
 Qed.
-- 
cgit v1.2.3