From b987bced399decd3b4247e2b4bb716d36846ee68 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Tue, 15 Dec 2020 19:02:03 -0800
Subject: Modify QArith/Qreduction.v to compile with -mangle-names

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

diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index 533c675415..e94ae1e789 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -129,19 +129,19 @@ Qed.
 
 Add Morphism Qplus' with signature (Qeq ==> Qeq ==> Qeq) as Qplus'_comp.
 Proof.
-  intros; unfold Qplus'.
+  intros ? ? H ? ? H0; unfold Qplus'.
   rewrite H, H0; auto with qarith.
 Qed.
 
 Add Morphism Qmult' with signature (Qeq ==> Qeq ==> Qeq) as Qmult'_comp.
 Proof.
-  intros; unfold Qmult'.
+  intros ? ? H ? ? H0; unfold Qmult'.
   rewrite H, H0; auto with qarith.
 Qed.
 
 Add Morphism Qminus' with signature (Qeq ==> Qeq ==> Qeq) as Qminus'_comp.
 Proof.
-  intros; unfold Qminus'.
+  intros ? ? H ? ? H0; unfold Qminus'.
   rewrite H, H0; auto with qarith.
 Qed.
 
-- 
cgit v1.2.3