From 74ff43a54315edb7da8c8512dcbdd9e4c88b8c45 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Sun, 5 Apr 2015 10:11:53 -0400
Subject: [PATCH] refactor(library/init/{funext,quot}.lean): adjust comments
 and headers

---
 library/init/funext.lean | 6 +++---
 library/init/quot.lean   | 3 ++-
 2 files changed, 5 insertions(+), 4 deletions(-)

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