diff --git a/library/init/funext.lean b/library/init/funext.lean
index acef03bf4..7a05a4883 100644
--- a/library/init/funext.lean
+++ b/library/init/funext.lean
@@ -2,21 +2,21 @@
 Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
+Module: init.funext
 Author: Jeremy Avigad
 
-function extensionality from quotients
+Function extensionality follows from quotients.
 -/
 prelude
 import init.quot init.logic
 
-/- function extensionality follows from quotients -/
 section
   open quot
   variables {A : Type} {B : A → Type}
 
   private definition fun_eqv (f₁ f₂ : Πx : A, B x) : Prop := ∀x, f₁ x = f₂ x
 
-  infix `~` := fun_eqv    -- this is "~"
+  infix `~` := fun_eqv
 
   private theorem fun_eqv.refl (f : Πx : A, B x) : f ~ f := take x, rfl
 
diff --git a/library/init/quot.lean b/library/init/quot.lean
index 4a1e465a7..83cd77a2d 100644
--- a/library/init/quot.lean
+++ b/library/init/quot.lean
@@ -2,9 +2,10 @@
 Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
+Module: init.quot
 Author: Leonardo de Moura
 
-Quotient types
+Quotient types.
 -/
 prelude
 import init.sigma init.setoid init.logic