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/rat.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v
index 393b37b..cd7d306 100644
--- a/mathcomp/algebra/rat.v
+++ b/mathcomp/algebra/rat.v
@@ -777,7 +777,7 @@ Qed.
 
 End InPrealField.
 
-Implicit Arguments ratr [[R]].
+Arguments ratr {R}.
 
 (* Conntecting rationals to the ring an field tactics *)
 
-- 
cgit v1.2.3