From f049e51c39077a025907ea87c08178dad1841801 Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Tue, 20 Nov 2018 17:51:11 +0100
Subject: Merge Arguments and Prenex Implicits

See the discussion here:
https://github.com/math-comp/math-comp/pull/242#discussion_r233778114
---
 mathcomp/ssreflect/div.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

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

diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index 6565ddf..ed1eedf 100644
--- a/mathcomp/ssreflect/div.v
+++ b/mathcomp/ssreflect/div.v
@@ -302,8 +302,7 @@ Proof.
 apply: (iffP eqP) => [md0 | [k ->]]; last by rewrite modnMl.
 by exists (m %/ d); rewrite {1}(divn_eq m d) md0 addn0.
 Qed.
-Arguments dvdnP [d m].
-Prenex Implicits dvdnP.
+Arguments dvdnP {d m}.
 
 Lemma dvdn0 d : d %| 0.
 Proof. by case: d. Qed.
-- 
cgit v1.2.3