From 19f9b3e774db1dedca149675f022d65cdeab7e6c Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Wed, 21 Feb 2018 22:41:00 -0800
Subject: Change Implicit Arguments to Arguments in ssreflect

---
 mathcomp/ssreflect/prime.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'mathcomp/ssreflect/prime.v')

diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index 9494353..648737b 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -349,8 +349,8 @@ case/primeP=> _ min_p d_neq1; apply: (iffP idP) => [/min_p|-> //].
 by rewrite (negPf d_neq1) /= => /eqP.
 Qed.
 
-Implicit Arguments primeP [p].
-Implicit Arguments primePn [n].
+Arguments primeP [p].
+Arguments primePn [n].
 Prenex Implicits primePn primeP.
 
 Lemma prime_gt1 p : prime p -> 1 < p.
@@ -541,7 +541,7 @@ exists (pdiv n); rewrite pdiv_dvd pdiv_prime //; split=> //.
 by case: leqP npr_p => //; move/ltn_pdiv2_prime->; auto.
 Qed.
 
-Implicit Arguments primePns [n].
+Arguments primePns [n].
 Prenex Implicits primePns.
 
 Lemma pdivP n : n > 1 -> {p | prime p & p %| n}.
-- 
cgit v1.2.3