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/zmodp.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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

diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v
index ec9750a..f9bdaaa 100644
--- a/mathcomp/algebra/zmodp.v
+++ b/mathcomp/algebra/zmodp.v
@@ -178,9 +178,9 @@ Proof. by rewrite orderE -Zp_cycle cardsT card_ord. Qed.
 
 End ZpDef.
 
-Implicit Arguments Zp0 [[p']].
-Implicit Arguments Zp1 [[p']].
-Implicit Arguments inZp [[p']].
+Arguments Zp0 {p'}.
+Arguments Zp1 {p'}.
+Arguments inZp {p'}.
 
 Lemma ord1 : all_equal_to (0 : 'I_1).
 Proof. by case=> [[] // ?]; apply: val_inj. Qed.
-- 
cgit v1.2.3