diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 67bb43c3b..698794d56 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -9,6 +9,8 @@
 ### Renamed
 
 ### Generalized
+- in `reals.v`:
+  + lemma `rat_in_itvoo`
 
 ### Deprecated
 
diff --git a/theories/reals.v b/theories/reals.v
index a989068bb..c2dd629c5 100644
--- a/theories/reals.v
+++ b/theories/reals.v
@@ -677,7 +677,7 @@ rewrite /bound_div (ltNge y 0) y0/= -mulr_natl -ltr_pdivrMr//.
 by rewrite archi_boundP// (divr_ge0 _(ltW _)).
 Qed.
 
-Lemma rat_in_itvoo (R : realType) (x y : R) :
+Lemma rat_in_itvoo (R : archiFieldType) (x y : R) :
   x < y -> exists q, ratr q \in `]x, y[.
 Proof.
 move=> xy; move: (xy); rewrite -subr_gt0.