aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/algebra/rat.v
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp/algebra/rat.v')
-rw-r--r--mathcomp/algebra/rat.v2
1 files changed, 1 insertions, 1 deletions
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 *)