diff --git a/src/data/fp/basic.lean b/src/data/fp/basic.lean
index deeee1f7cb639..613875501a11a 100644
--- a/src/data/fp/basic.lean
+++ b/src/data/fp/basic.lean
@@ -2,11 +2,12 @@
 Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
-
-Implementation of floating-point numbers (experimental).
 -/
 import data.rat
 import data.semiquot
+/-!
+# Implementation of floating-point numbers (experimental).
+-/
 
 def int.shift2 (a b : ℕ) : ℤ → ℕ × ℕ
 | (int.of_nat e) := (a.shiftl e, b)