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

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

diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index 040b3a8..34174bf 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -1688,11 +1688,11 @@ Notation "a ^` ()" := (deriv a) : ring_scope.
 Notation "a ^` ( n )" := (derivn n a) : ring_scope.
 Notation "a ^`N ( n )" := (nderivn n a) : ring_scope.
 
-Arguments monicP [R p].
-Arguments rootP [R p x].
-Arguments rootPf [R p x].
-Arguments rootPt [R p x].
-Arguments unity_rootP [R n z].
+Arguments monicP {R p}.
+Arguments rootP {R p x}.
+Arguments rootPf {R p x}.
+Arguments rootPt {R p x}.
+Arguments unity_rootP {R n z}.
 Arguments polyOverP {R S0 addS kS p}.
 
 Canonical polynomial_countZmodType (R : countRingType) :=
@@ -2611,7 +2611,7 @@ Open Scope unity_root_scope.
 
 Definition unity_rootE := unity_rootE.
 Definition unity_rootP := @unity_rootP.
-Arguments unity_rootP [R n z].
+Arguments unity_rootP {R n z}.
 
 Definition prim_order_exists := prim_order_exists.
 Notation prim_order_gt0 :=  prim_order_gt0.
-- 
cgit v1.2.3