diff --git a/library/data/real/real.md b/library/data/real/real.md
index d9a17fdf8..2acde23a7 100644
--- a/library/data/real/real.md
+++ b/library/data/real/real.md
@@ -3,4 +3,6 @@ data.real
 
 The real numbers.
 
-* [basic](basic.lean) : the reals as a commutative ring
\ No newline at end of file
+* [basic](basic.lean) : the reals as a commutative ring (constructive)
+* [order](order.lean) : the reals as an ordered ring (constructive)
+* [division](division.lean) : the reals as a discrete linear ordered field (classical)
\ No newline at end of file