diff --git a/library/algebra/binary.lean b/library/algebra/binary.lean
index 078e25cb0..1af950118 100644
--- a/library/algebra/binary.lean
+++ b/library/algebra/binary.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: algebra.binary
 Authors: Leonardo de Moura, Jeremy Avigad
 
 General properties of binary operations.
diff --git a/library/algebra/bundled.lean b/library/algebra/bundled.lean
index ea41110d5..94efaa25f 100644
--- a/library/algebra/bundled.lean
+++ b/library/algebra/bundled.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2015 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: algebra.bundled
 Authors: Jeremy Avigad
 
 Bundled structures
diff --git a/library/algebra/category/adjoint.lean b/library/algebra/category/adjoint.lean
index bb41d6014..88c7bf067 100644
--- a/library/algebra/category/adjoint.lean
+++ b/library/algebra/category/adjoint.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: algebra.category.adjoint
 Author: Floris van Doorn
 -/
 
diff --git a/library/algebra/category/basic.lean b/library/algebra/category/basic.lean
index c165a8a67..d2176572d 100644
--- a/library/algebra/category/basic.lean
+++ b/library/algebra/category/basic.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: algebra.category.basic
 Author: Floris van Doorn
 -/
 open eq eq.ops
diff --git a/library/algebra/category/default.lean b/library/algebra/category/default.lean
index e5656b3ed..7c35a9c4e 100644
--- a/library/algebra/category/default.lean
+++ b/library/algebra/category/default.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: algebra.category.default
 Author: Floris van Doorn
 -/
 
diff --git a/library/algebra/category/functor.lean b/library/algebra/category/functor.lean
index 580f18ae8..d07f9f33a 100644
--- a/library/algebra/category/functor.lean
+++ b/library/algebra/category/functor.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: algebra.category.functor
 Author: Floris van Doorn
 -/
 import .basic
diff --git a/library/algebra/category/limit.lean b/library/algebra/category/limit.lean
index 41c726f22..1ac6aea04 100644
--- a/library/algebra/category/limit.lean
+++ b/library/algebra/category/limit.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: algebra.category.limit
 Author: Floris van Doorn
 -/
 
diff --git a/library/algebra/category/morphism.lean b/library/algebra/category/morphism.lean
index a1f8616a3..97ffc91e0 100644
--- a/library/algebra/category/morphism.lean
+++ b/library/algebra/category/morphism.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: algebra.category.morphism
 Author: Floris van Doorn
 -/
 
diff --git a/library/algebra/category/natural_transformation.lean b/library/algebra/category/natural_transformation.lean
index 184e4732b..1357b3a56 100644
--- a/library/algebra/category/natural_transformation.lean
+++ b/library/algebra/category/natural_transformation.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: algebra.category.natural_transformation
 Author: Floris van Doorn
 -/
 
diff --git a/library/algebra/category/yoneda.lean b/library/algebra/category/yoneda.lean
index 7d1983b08..75f0c7f35 100644
--- a/library/algebra/category/yoneda.lean
+++ b/library/algebra/category/yoneda.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: algebra.category.yoneda
 Author: Floris van Doorn
 -/
 
diff --git a/library/algebra/field.lean b/library/algebra/field.lean
index 6fa18d27c..2f8e441d1 100644
--- a/library/algebra/field.lean
+++ b/library/algebra/field.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Robert Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: algebra.field
 Authors: Robert Lewis
 
 Structures with multiplicative and additive components, including division rings and fields.
diff --git a/library/algebra/function.lean b/library/algebra/function.lean
index c7ef29668..62a64d6ea 100644
--- a/library/algebra/function.lean
+++ b/library/algebra/function.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: algebra.function
 Author: Leonardo de Moura
 
 General operations on functions.
diff --git a/library/algebra/order.lean b/library/algebra/order.lean
index b57b69d55..891e35e74 100644
--- a/library/algebra/order.lean
+++ b/library/algebra/order.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: algebra.order
 Author: Jeremy Avigad
 
 Various types of orders. We develop weak orders "≤" and strict orders "<" separately. We also
diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean
index 8186fdd5d..dd212a40c 100644
--- a/library/algebra/ordered_field.lean
+++ b/library/algebra/ordered_field.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Robert Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: algebra.ordered_field
 Authors: Robert Lewis
 
 -/
diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean
index 015dc583c..e90de0994 100644
--- a/library/algebra/ordered_group.lean
+++ b/library/algebra/ordered_group.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: algebra.ordered_group
 Authors: Jeremy Avigad
 
 Partially ordered additive groups, modeled on Isabelle's library. We could refine the structures,
diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean
index a0e1cc12a..916449d2b 100644
--- a/library/algebra/ordered_ring.lean
+++ b/library/algebra/ordered_ring.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: algebra.ordered_ring
 Authors: Jeremy Avigad
 
 Here an "ordered_ring" is partially ordered ring, which is ordered with respect to both a weak
diff --git a/library/algebra/relation.lean b/library/algebra/relation.lean
index 3582439c8..e30160483 100644
--- a/library/algebra/relation.lean
+++ b/library/algebra/relation.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: algebra.relation
 Author: Jeremy Avigad
 
 General properties of relations, and classes for equivalence relations and congruences.
diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean
index 30d73d14d..0bd34368b 100644
--- a/library/algebra/ring.lean
+++ b/library/algebra/ring.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: algebra.ring
 Authors: Jeremy Avigad, Leonardo de Moura
 
 Structures with multiplicative and additive components, including semirings, rings, and fields.
diff --git a/library/classical.lean b/library/classical.lean
index a0b1c7478..fb497f98f 100644
--- a/library/classical.lean
+++ b/library/classical.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: classical
 Author: Jeremy Avigad
 
 The standard library together with the classical axioms.
diff --git a/library/data/bool.lean b/library/data/bool.lean
index e4ed2e71c..5240abfe7 100644
--- a/library/data/bool.lean
+++ b/library/data/bool.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.bool
 Author: Leonardo de Moura
 -/
 
diff --git a/library/data/countable.lean b/library/data/countable.lean
index dda63c468..2f1a330ef 100644
--- a/library/data/countable.lean
+++ b/library/data/countable.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.countable
 Author: Leonardo de Moura
 
 Define countable types
diff --git a/library/data/empty.lean b/library/data/empty.lean
index 7f5eb70fc..0ed1583e2 100644
--- a/library/data/empty.lean
+++ b/library/data/empty.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.empty
 Author: Jeremy Avigad, Floris van Doorn
 -/
 import logic.cast
diff --git a/library/data/encodable.lean b/library/data/encodable.lean
index 706bdd40b..0c2bafc0a 100644
--- a/library/data/encodable.lean
+++ b/library/data/encodable.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.encodable
 Author: Leonardo de Moura
 
 Type class for encodable types.
diff --git a/library/data/examples/depchoice.lean b/library/data/examples/depchoice.lean
index f961cc24e..83afb8eeb 100644
--- a/library/data/examples/depchoice.lean
+++ b/library/data/examples/depchoice.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.examples.depchoice
 Author: Leonardo de Moura
 -/
 import data.encodable
diff --git a/library/data/examples/notencodable.lean b/library/data/examples/notencodable.lean
index e1397f5cc..c75142084 100644
--- a/library/data/examples/notencodable.lean
+++ b/library/data/examples/notencodable.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.examples.unencodable
 Author: Leonardo de Moura
 
 Small example showing that (nat → nat) is not encodable.
diff --git a/library/data/fin.lean b/library/data/fin.lean
index 48fb2fbd9..0858447d7 100644
--- a/library/data/fin.lean
+++ b/library/data/fin.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.fin
 Author: Leonardo de Moura
 
 Finite ordinals.
diff --git a/library/data/int/default.lean b/library/data/int/default.lean
index be7f58b17..19b0463ac 100644
--- a/library/data/int/default.lean
+++ b/library/data/int/default.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.int.default
 Author: Jeremy Avigad
 -/
 import .basic .order .div .power
diff --git a/library/data/int/div.lean b/library/data/int/div.lean
index 112a6b83c..386f6023e 100644
--- a/library/data/int/div.lean
+++ b/library/data/int/div.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.int.div
 Author: Jeremy Avigad
 
 Definitions and properties of div, mod, gcd, lcm, coprime, following the SSReflect library.
diff --git a/library/data/list/as_type.lean b/library/data/list/as_type.lean
index 83ec2cc58..9fc80f3b1 100644
--- a/library/data/list/as_type.lean
+++ b/library/data/list/as_type.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2015 Leonardo de Moura. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.list.as_type
 Authors: Leonardo de Moura
 -/
 import data.list.basic
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index dc9fcc9ae..5f21a439d 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Parikshit Khanna. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.list.basic
 Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura
 
 Basic properties of lists.
diff --git a/library/data/nat/bquant.lean b/library/data/nat/bquant.lean
index 6bc962da2..2e3ff1ff3 100644
--- a/library/data/nat/bquant.lean
+++ b/library/data/nat/bquant.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.nat.bquant
 Author: Leonardo de Moura
 
 Show that "bounded" quantifiers: (∃x, x < n ∧ P x) and (∀x, x < n → P x)
diff --git a/library/data/nat/choose.lean b/library/data/nat/choose.lean
index b8d9a4952..9b86fed3a 100644
--- a/library/data/nat/choose.lean
+++ b/library/data/nat/choose.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.nat.choose
 Authors: Leonardo de Moura
 
 Choice function for decidable predicates on natural numbers.
diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index 14922c74d..00d057e65 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.nat.div
 Authors: Jeremy Avigad, Leonardo de Moura
 
 Definitions and properties of div, mod, gcd, lcm, coprime. Much of the development follows
diff --git a/library/data/nat/pairing.lean b/library/data/nat/pairing.lean
index 369a753f2..4a3356467 100644
--- a/library/data/nat/pairing.lean
+++ b/library/data/nat/pairing.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.nat.pairing
 Authors: Leonardo de Moura
 
 Elegant pairing function.
diff --git a/library/data/nat/sqrt.lean b/library/data/nat/sqrt.lean
index c051e773a..295ebda8f 100644
--- a/library/data/nat/sqrt.lean
+++ b/library/data/nat/sqrt.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.nat.sqrt
 Authors: Leonardo de Moura
 
 Very simple (sqrt n) function that returns s s.t.
diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean
index 2b3a67df9..fa5c3d8b5 100644
--- a/library/data/nat/sub.lean
+++ b/library/data/nat/sub.lean
@@ -3,8 +3,6 @@ Copyright (c) 2014 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Authors: Floris van Doorn, Jeremy Avigad
-Module: data.nat.sub
-
 Subtraction on the natural numbers, as well as min, max, and distance.
 -/
 import .order
diff --git a/library/data/num.lean b/library/data/num.lean
index 0662e05f7..758d95c8b 100644
--- a/library/data/num.lean
+++ b/library/data/num.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.num
 Author: Leonardo de Moura
 -/
 import data.bool tools.helper_tactics
diff --git a/library/data/option.lean b/library/data/option.lean
index 1aada7052..bf15efd78 100644
--- a/library/data/option.lean
+++ b/library/data/option.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.option
 Author: Leonardo de Moura
 -/
 
diff --git a/library/data/prod.lean b/library/data/prod.lean
index 7daf6ad47..1e0198029 100644
--- a/library/data/prod.lean
+++ b/library/data/prod.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.prod
 Author: Leonardo de Moura, Jeremy Avigad
 -/
 import logic.eq
diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean
index d0982cd8f..3c0966de7 100644
--- a/library/data/rat/basic.lean
+++ b/library/data/rat/basic.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.rat.basic
 Author: Jeremy Avigad
 
 The rational numbers as a field generated by the integers, defined as the usual quotient.
diff --git a/library/data/rat/order.lean b/library/data/rat/order.lean
index b0e39f5f2..e43ab8af8 100644
--- a/library/data/rat/order.lean
+++ b/library/data/rat/order.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2015 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.rat.order
 Author: Jeremy Avigad
 
 Adds the ordering, and instantiates the rationals as an ordered field.
diff --git a/library/data/set/classical_inverse.lean b/library/data/set/classical_inverse.lean
index ac1d6b4db..37f350a46 100644
--- a/library/data/set/classical_inverse.lean
+++ b/library/data/set/classical_inverse.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.set.function
 Author: Jeremy Avigad, Andrew Zipperer
 
 Using classical logic, defines an inverse function.
diff --git a/library/data/set/default.lean b/library/data/set/default.lean
index 600339d23..b10e1aead 100644
--- a/library/data/set/default.lean
+++ b/library/data/set/default.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.set.default
 Author: Jeremy Avigad
 -/
 import .basic .function .map
diff --git a/library/data/set/function.lean b/library/data/set/function.lean
index 0ee35ec5d..53d7c12f2 100644
--- a/library/data/set/function.lean
+++ b/library/data/set/function.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.set.function
 Author: Jeremy Avigad, Andrew Zipperer, Haitao Zhang
 
 Functions between subsets of finite types.
diff --git a/library/data/set/map.lean b/library/data/set/map.lean
index 2a1878004..52de59ebd 100644
--- a/library/data/set/map.lean
+++ b/library/data/set/map.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.set.map
 Author: Jeremy Avigad, Andrew Zipperer
 
 Functions between subsets of finite types, bundled with the domain and range.
diff --git a/library/data/sigma.lean b/library/data/sigma.lean
index 98fb47c2e..5658e1e54 100644
--- a/library/data/sigma.lean
+++ b/library/data/sigma.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.sigma
 Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
 
 Sigma types, aka dependent sum.
diff --git a/library/data/squash.lean b/library/data/squash.lean
index 2ef9b48cb..c13c72c05 100644
--- a/library/data/squash.lean
+++ b/library/data/squash.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.squash
 Author: Leonardo de Moura
 
 Define squash type (aka propositional truncation) using quotients.
diff --git a/library/data/stream.lean b/library/data/stream.lean
index 15fc2016a..46ab07e44 100644
--- a/library/data/stream.lean
+++ b/library/data/stream.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.stream
 Author: Leonardo de Moura
 -/
 import data.nat
diff --git a/library/data/string.lean b/library/data/string.lean
index 49971a69d..5efce9b5a 100644
--- a/library/data/string.lean
+++ b/library/data/string.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.string
 Author: Leonardo de Moura
 -/
 import data.bool
diff --git a/library/data/subtype.lean b/library/data/subtype.lean
index a97f4b52e..6aa894fb4 100644
--- a/library/data/subtype.lean
+++ b/library/data/subtype.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.subtype
 Author: Leonardo de Moura, Jeremy Avigad
 -/
 
diff --git a/library/data/sum.lean b/library/data/sum.lean
index ed0fe4973..10d3d9948 100644
--- a/library/data/sum.lean
+++ b/library/data/sum.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.sum
 Authors: Leonardo de Moura, Jeremy Avigad
 
 The sum type, aka disjoint union.
diff --git a/library/data/unit.lean b/library/data/unit.lean
index b48be9e2e..4d340112b 100644
--- a/library/data/unit.lean
+++ b/library/data/unit.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.unit
 Author: Leonardo de Moura
 -/
 import logic.eq
diff --git a/library/data/uprod.lean b/library/data/uprod.lean
index ee46b9f7c..44c428218 100644
--- a/library/data/uprod.lean
+++ b/library/data/uprod.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.uprod
 Author: Leonardo de Moura
 
 Unordered pairs
diff --git a/library/data/vector.lean b/library/data/vector.lean
index c3c1130b6..a46e90e0c 100644
--- a/library/data/vector.lean
+++ b/library/data/vector.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.vector
 Author: Floris van Doorn, Leonardo de Moura
 -/
 import data.nat data.list data.fin
diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean
index 00f7dbf12..89732ca91 100644
--- a/library/init/datatypes.lean
+++ b/library/init/datatypes.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: init.datatypes
 Authors: Leonardo de Moura
 
 Basic datatypes
diff --git a/library/init/default.lean b/library/init/default.lean
index 829456fbc..98a54c91e 100644
--- a/library/init/default.lean
+++ b/library/init/default.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: init.default
 Authors: Leonardo de Moura
 -/
 prelude
diff --git a/library/init/funext.lean b/library/init/funext.lean
index 73dc630e8..6dbbb5207 100644
--- a/library/init/funext.lean
+++ b/library/init/funext.lean
@@ -1,8 +1,6 @@
 /-
 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
 
 Extensional equality for functions, and a proof of function extensionality from quotients.
diff --git a/library/init/logic.lean b/library/init/logic.lean
index d74d6e050..022be6bd1 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: init.logic
 Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
 -/
 prelude
diff --git a/library/init/measurable.lean b/library/init/measurable.lean
index aafc2f3cd..97dab5094 100644
--- a/library/init/measurable.lean
+++ b/library/init/measurable.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: init.measurable
 Authors: Leonardo de Moura
 
 Types with a nat-valued complexity measure.
diff --git a/library/init/nat.lean b/library/init/nat.lean
index 621df7f7d..7914bf340 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: init.nat
 Authors: Floris van Doorn, Leonardo de Moura
 -/
 prelude
diff --git a/library/init/num.lean b/library/init/num.lean
index d26a84f1c..ca83897be 100644
--- a/library/init/num.lean
+++ b/library/init/num.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: init.num
 Authors: Leonardo de Moura
 -/
 
diff --git a/library/init/priority.lean b/library/init/priority.lean
index 705ecd779..27d671129 100644
--- a/library/init/priority.lean
+++ b/library/init/priority.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: init.priority
 Authors: Leonardo de Moura
 -/
 prelude
diff --git a/library/init/prod.lean b/library/init/prod.lean
index a29ec3dce..34e7ca7be 100644
--- a/library/init/prod.lean
+++ b/library/init/prod.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: init.prod
 Author: Leonardo de Moura, Jeremy Avigad
 -/
 prelude
diff --git a/library/init/quot.lean b/library/init/quot.lean
index dd5c4c937..5a283b47c 100644
--- a/library/init/quot.lean
+++ b/library/init/quot.lean
@@ -1,8 +1,6 @@
 /-
 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.
diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean
index 7ed4ce1ae..b08af371c 100644
--- a/library/init/reserved_notation.lean
+++ b/library/init/reserved_notation.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: init.reserved_notation
 Authors: Leonardo de Moura, Jeremy Avigad
 -/
 prelude
diff --git a/library/init/sigma.lean b/library/init/sigma.lean
index fbc810a30..3a7f02601 100644
--- a/library/init/sigma.lean
+++ b/library/init/sigma.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: init.sigma
 Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
 -/
 prelude
diff --git a/library/init/tactic.lean b/library/init/tactic.lean
index fe05fbf69..d8f2e70a4 100644
--- a/library/init/tactic.lean
+++ b/library/init/tactic.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: init.tactic
 Author: Leonardo de Moura
 
 This is just a trick to embed the 'tactic language' as a Lean
diff --git a/library/init/wf.lean b/library/init/wf.lean
index c6abc70da..e0e101c04 100644
--- a/library/init/wf.lean
+++ b/library/init/wf.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: init.wf
 Author: Leonardo de Moura
 -/
 prelude
diff --git a/library/logic/axioms/classical.lean b/library/logic/axioms/classical.lean
index 773535444..bc834761d 100644
--- a/library/logic/axioms/classical.lean
+++ b/library/logic/axioms/classical.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: logic.axioms.classical
 Author: Jeremy Avigad
 -/
 import logic.axioms.prop_complete logic.axioms.hilbert
diff --git a/library/logic/axioms/em.lean b/library/logic/axioms/em.lean
index 4d9a67268..7b644e359 100644
--- a/library/logic/axioms/em.lean
+++ b/library/logic/axioms/em.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: logic.axioms.funext
 Author: Leonardo de Moura
 
 Excluded middle
diff --git a/library/logic/axioms/hilbert.lean b/library/logic/axioms/hilbert.lean
index 893fa62f5..70eaa0aa0 100644
--- a/library/logic/axioms/hilbert.lean
+++ b/library/logic/axioms/hilbert.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: logic.axioms.hilbert
 Authors: Leonardo de Moura, Jeremy Avigad
 
 Follows Coq.Logic.ClassicalEpsilon (but our definition of "inhabited" is the constructive one).
diff --git a/library/logic/axioms/prop_complete.lean b/library/logic/axioms/prop_complete.lean
index 2c1f4a7d1..2b9ef8e5c 100644
--- a/library/logic/axioms/prop_complete.lean
+++ b/library/logic/axioms/prop_complete.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: logic.axioms.classical
 Author: Leonardo de Moura
 -/
 import logic.connectives logic.quantifiers logic.cast algebra.relation
diff --git a/library/logic/axioms/prop_decidable.lean b/library/logic/axioms/prop_decidable.lean
index 14daeeb83..02e73171b 100644
--- a/library/logic/axioms/prop_decidable.lean
+++ b/library/logic/axioms/prop_decidable.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: logic.axioms.prop_decidable
 Author: Leonardo de Moura
 
 Excluded middle + Hilbert implies every proposition is decidable.
diff --git a/library/logic/cast.lean b/library/logic/cast.lean
index 54d48e997..6d90638b2 100644
--- a/library/logic/cast.lean
+++ b/library/logic/cast.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: cast.lean
 Author: Leonardo de Moura
 
 Casts and heterogeneous equality. See also init.datatypes and init.logic.
diff --git a/library/logic/default.lean b/library/logic/default.lean
index 8353bc33c..fc251202e 100644
--- a/library/logic/default.lean
+++ b/library/logic/default.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: logic.default
 Author: Jeremy Avigad
 -/
 import logic.eq logic.connectives logic.cast
diff --git a/library/logic/eq.lean b/library/logic/eq.lean
index a527a4c75..19570c48a 100644
--- a/library/logic/eq.lean
+++ b/library/logic/eq.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: logic.eq
 Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
 
 Additional declarations/theorems about equality. See also init.datatypes and init.logic.
diff --git a/library/logic/examples/instances_test.lean b/library/logic/examples/instances_test.lean
index 1bb7e9d59..c0181cb1f 100644
--- a/library/logic/examples/instances_test.lean
+++ b/library/logic/examples/instances_test.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: logic.examples.instances_test
 Author: Jeremy Avigad
 
 Illustrates substitution and congruence with iff.
diff --git a/library/logic/identities.lean b/library/logic/identities.lean
index 799fcb96c..d94309aae 100644
--- a/library/logic/identities.lean
+++ b/library/logic/identities.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: logic.identities
 Authors: Jeremy Avigad, Leonardo de Moura
 
 Useful logical identities. Since we are not using propositional extensionality, some of the
diff --git a/library/logic/instances.lean b/library/logic/instances.lean
index 42e10b7e4..e9ac41a61 100644
--- a/library/logic/instances.lean
+++ b/library/logic/instances.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: logic.instances
 Author: Jeremy Avigad
 
 Class instances for iff and eq.
diff --git a/library/logic/quantifiers.lean b/library/logic/quantifiers.lean
index f9eeb3a19..357528cfc 100644
--- a/library/logic/quantifiers.lean
+++ b/library/logic/quantifiers.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: logic.quantifiers
 Authors: Leonardo de Moura, Jeremy Avigad
 
 Universal and existential quantifiers. See also init.logic.
diff --git a/library/standard.lean b/library/standard.lean
index d933fa7d4..82b228ac3 100644
--- a/library/standard.lean
+++ b/library/standard.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: standard
 Authors: Leonardo de Moura, Jeremy Avigad
 
 The constructive core of Lean's library.
diff --git a/tests/lean/run/finbug.lean b/tests/lean/run/finbug.lean
index 5ddec75d0..39b7cd226 100644
--- a/tests/lean/run/finbug.lean
+++ b/tests/lean/run/finbug.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.fin
 Author: Leonardo de Moura
 
 Finite ordinals.
diff --git a/tests/lean/run/finbug2.lean b/tests/lean/run/finbug2.lean
index 31c3a3233..bcaf3b519 100644
--- a/tests/lean/run/finbug2.lean
+++ b/tests/lean/run/finbug2.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.fin
 Author: Leonardo de Moura
 
 Finite ordinals.