jdchristensen

diff --git a/theories/Classes/implementations/field_of_fractions.v b/theories/Classes/implementations/field_of_fractions.v
index 853f5f748..015b3e17a 100644
--- a/theories/Classes/implementations/field_of_fractions.v
+++ b/theories/Classes/implementations/field_of_fractions.v
@@ -301,12 +301,13 @@ Definition F_rec_compute T sT dclass dequiv x
   : @F_rec T sT dclass dequiv (' x) = dclass x
   := 1.
 
-Definition F_rec2@{i j} {T:Type@{i} } {sT : IsHSet T}
+Definition F_rec2@{i} {T:Type@{i} } {sT : IsHSet T}