From 64ceb784611e5ded0c715835a36490de1c3bb1ca Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Wed, 21 Feb 2018 23:27:04 -0800
Subject: Change Implicit Arguments to Arguments in algebra

---
 mathcomp/algebra/interval.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/algebra/interval.v')

diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v
index e269752..b699da1 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.v
@@ -134,7 +134,7 @@ Lemma itv_dec : forall (x : R) (i : interval R),
   reflect (itv_decompose i x) (x \in i).
 Proof. by move=> x [[[] a|] [[] b|]]; apply: (iffP andP); case. Qed.
 
-Implicit Arguments itv_dec [x i].
+Arguments itv_dec [x i].
 
 Definition lersif (x y : R) b := if b then x < y else x <= y.
 
@@ -243,7 +243,7 @@ move=> x [[[] a|] [[] b|]]; move/itv_dec=> //= [hl hu]; do ?[split=> //;
 Qed.
 
 Hint Rewrite intP.
-Implicit Arguments itvP [x i].
+Arguments itvP [x i].
 
 Definition subitv (i1 i2 : interval R) :=
   match i1, i2 with
-- 
cgit v1.2.3