From 9a55d469042cef943dd0be20083896741a1c5dcc Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Thu, 8 Oct 2020 17:01:48 -0700
Subject: Modify Numbers/Integer/Abstract/ZAddOrder.v to compile with
 -mangle-names

---
 theories/Numbers/Integer/Abstract/ZAddOrder.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'theories/Numbers/Integer')

diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v
index 40a37be5f9..5a293c6483 100644
--- a/theories/Numbers/Integer/Abstract/ZAddOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v
@@ -241,25 +241,25 @@ Qed.
 
 Theorem sub_neg_cases : forall n m, n - m < 0 -> n < 0 \/ 0 < m.
 Proof.
-intros.
+intros n m ?.
 rewrite <- (opp_neg_pos m). apply add_neg_cases. now rewrite add_opp_r.
 Qed.
 
 Theorem sub_pos_cases : forall n m, 0 < n - m -> 0 < n \/ m < 0.
 Proof.
-intros.
+intros n m ?.
 rewrite <- (opp_pos_neg m). apply add_pos_cases. now rewrite add_opp_r.
 Qed.
 
 Theorem sub_nonpos_cases : forall n m, n - m <= 0 -> n <= 0 \/ 0 <= m.
 Proof.
-intros.
+intros n m ?.
 rewrite <- (opp_nonpos_nonneg m). apply add_nonpos_cases. now rewrite add_opp_r.
 Qed.
 
 Theorem sub_nonneg_cases : forall n m, 0 <= n - m -> 0 <= n \/ m <= 0.
 Proof.
-intros.
+intros n m ?.
 rewrite <- (opp_nonneg_nonpos m). apply add_nonneg_cases. now rewrite add_opp_r.
 Qed.
 
-- 
cgit v1.2.3