diff --git a/src/data/polynomial/field_division.lean b/src/data/polynomial/field_division.lean
index 7f46976d33b2a..9dcf370525e68 100644
--- a/src/data/polynomial/field_division.lean
+++ b/src/data/polynomial/field_division.lean
@@ -1,4 +1,3 @@
-
 /-
 Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
diff --git a/src/data/polynomial/integral_normalization.lean b/src/data/polynomial/integral_normalization.lean
index 5199de1781956..05c3df02a5c30 100644
--- a/src/data/polynomial/integral_normalization.lean
+++ b/src/data/polynomial/integral_normalization.lean
@@ -1,4 +1,3 @@
-
 /-
 Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
diff --git a/src/data/set/function.lean b/src/data/set/function.lean
index 3e8f99ea91d5e..4d1aa8fdc07e3 100644
--- a/src/data/set/function.lean
+++ b/src/data/set/function.lean
@@ -1,4 +1,4 @@
-  /-
+/-
 Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Jeremy Avigad, Andrew Zipperer, Haitao Zhang, Minchao Wu, Yury Kudryashov
diff --git a/src/measure_theory/category/Meas.lean b/src/measure_theory/category/Meas.lean
index c4e83c8bf0423..328dfac331bb7 100644
--- a/src/measure_theory/category/Meas.lean
+++ b/src/measure_theory/category/Meas.lean
@@ -1,4 +1,5 @@
-/- Copyright (c) 2018 Johannes Hölzl. All rights reserved.
+/-
+Copyright (c) 2018 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
diff --git a/src/tactic/derive_fintype.lean b/src/tactic/derive_fintype.lean
index 9a94945edbf1b..be34264d71c4b 100644
--- a/src/tactic/derive_fintype.lean
+++ b/src/tactic/derive_fintype.lean
@@ -1,6 +1,7 @@
 /-
 Copyright (c) 2020 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
 -/
 import logic.basic
 import data.fintype.basic
diff --git a/src/tactic/derive_inhabited.lean b/src/tactic/derive_inhabited.lean
index a774f595656d2..848db5114f519 100644
--- a/src/tactic/derive_inhabited.lean
+++ b/src/tactic/derive_inhabited.lean
@@ -1,6 +1,7 @@
 /-
 Copyright (c) 2020 Gabriel Ebner. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner
 -/
 import logic.basic
 
diff --git a/src/tactic/interactive.lean b/src/tactic/interactive.lean
index 10a3cfda8d1b4..1c31bbc3cb4ca 100644
--- a/src/tactic/interactive.lean
+++ b/src/tactic/interactive.lean
@@ -1,4 +1,3 @@
-
 /-
 Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
diff --git a/src/tactic/omega/clause.lean b/src/tactic/omega/clause.lean
index e54a872118b0d..9d9c06e1ed928 100644
--- a/src/tactic/omega/clause.lean
+++ b/src/tactic/omega/clause.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+Definition of linear constrain clauses.
+-/
 
-Definition of linear constrain clauses. -/
 import tactic.omega.term
 
 namespace omega
diff --git a/src/tactic/omega/coeffs.lean b/src/tactic/omega/coeffs.lean
index 769ca23c08e6b..1aa233e78a758 100644
--- a/src/tactic/omega/coeffs.lean
+++ b/src/tactic/omega/coeffs.lean
@@ -1,9 +1,14 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
 
+/-
 Non-constant terms of linear constraints are represented
-by storing their coefficients in integer lists. -/
+by storing their coefficients in integer lists.
+-/
+
 import data.list.func
 import tactic.ring
 import tactic.omega.misc
diff --git a/src/tactic/omega/eq_elim.lean b/src/tactic/omega/eq_elim.lean
index d1c442e9cc17f..7245b7bcced20 100644
--- a/src/tactic/omega/eq_elim.lean
+++ b/src/tactic/omega/eq_elim.lean
@@ -1,9 +1,14 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
 
+/-
 Correctness lemmas for equality elimination.
-See 5.5 of <http://www.decision-procedures.org/> for details. -/
+See 5.5 of <http://www.decision-procedures.org/> for details.
+-/
+
 import tactic.omega.clause
 
 open list.func
diff --git a/src/tactic/omega/find_ees.lean b/src/tactic/omega/find_ees.lean
index 8c90d658ed6fc..b5be8c3a58484 100644
--- a/src/tactic/omega/find_ees.lean
+++ b/src/tactic/omega/find_ees.lean
@@ -1,9 +1,14 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
 
+/-
 A tactic for finding a sequence of equality
-elimination rules for a given set of constraints. -/
+elimination rules for a given set of constraints.
+-/
+
 import tactic.omega.eq_elim
 
 variables {α β : Type}
diff --git a/src/tactic/omega/find_scalars.lean b/src/tactic/omega/find_scalars.lean
index aa1aa22653f7e..91149b372c80c 100644
--- a/src/tactic/omega/find_scalars.lean
+++ b/src/tactic/omega/find_scalars.lean
@@ -1,9 +1,14 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
 
+/-
 Tactic for performing Fourier–Motzkin elimination to find
-a contradictory linear combination of input constraints. -/
+a contradictory linear combination of input constraints.
+-/
+
 import tactic.omega.term
 import data.list.min_max
 
diff --git a/src/tactic/omega/int/dnf.lean b/src/tactic/omega/int/dnf.lean
index 561ba2f5019b7..4773eb79d4447 100644
--- a/src/tactic/omega/int/dnf.lean
+++ b/src/tactic/omega/int/dnf.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+DNF transformation.
+-/
 
-DNF transformation. -/
 import tactic.omega.clause
 import tactic.omega.int.form
 
diff --git a/src/tactic/omega/int/form.lean b/src/tactic/omega/int/form.lean
index 4de2b5889b9a9..0a4f73b71c777 100644
--- a/src/tactic/omega/int/form.lean
+++ b/src/tactic/omega/int/form.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+Linear integer arithmetic formulas in pre-normalized form.
+-/
 
-Linear integer arithmetic formulas in pre-normalized form. -/
 import tactic.omega.int.preterm
 
 namespace omega
diff --git a/src/tactic/omega/int/main.lean b/src/tactic/omega/int/main.lean
index 05db7deacc858..3f4a19eda0a36 100644
--- a/src/tactic/omega/int/main.lean
+++ b/src/tactic/omega/int/main.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+Main procedure for linear integer arithmetic.
+-/
 
-Main procedure for linear integer arithmetic. -/
 import tactic.omega.prove_unsats
 import tactic.omega.int.dnf
 
diff --git a/src/tactic/omega/int/preterm.lean b/src/tactic/omega/int/preterm.lean
index 3ac51ba3e14a6..3936d85c9df91 100644
--- a/src/tactic/omega/int/preterm.lean
+++ b/src/tactic/omega/int/preterm.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+Linear integer arithmetic terms in pre-normalized form.
+-/
 
-Linear integer arithmetic terms in pre-normalized form. -/
 import tactic.omega.term
 
 namespace omega
diff --git a/src/tactic/omega/lin_comb.lean b/src/tactic/omega/lin_comb.lean
index d4dbbf6659452..b263c71427841 100644
--- a/src/tactic/omega/lin_comb.lean
+++ b/src/tactic/omega/lin_comb.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+Linear combination of constraints.
+-/
 
-Linear combination of constraints. -/
 import tactic.omega.clause
 
 namespace omega
diff --git a/src/tactic/omega/main.lean b/src/tactic/omega/main.lean
index 353ae30833ca1..e2b6b50acfb71 100644
--- a/src/tactic/omega/main.lean
+++ b/src/tactic/omega/main.lean
@@ -1,9 +1,14 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
 
+/-
 A tactic for discharging linear integer & natural
-number arithmetic goals using the Omega test. -/
+number arithmetic goals using the Omega test.
+-/
+
 import tactic.omega.int.main
 import tactic.omega.nat.main
 
diff --git a/src/tactic/omega/misc.lean b/src/tactic/omega/misc.lean
index c1eacdee140dd..64718d92e33f9 100644
--- a/src/tactic/omega/misc.lean
+++ b/src/tactic/omega/misc.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+Miscellaneous.
+-/
 
-Miscellaneous. -/
 import tactic.localized
 
 variables {α β γ : Type}
diff --git a/src/tactic/omega/nat/dnf.lean b/src/tactic/omega/nat/dnf.lean
index ba1b26ca7f32a..d038bde30e5bf 100644
--- a/src/tactic/omega/nat/dnf.lean
+++ b/src/tactic/omega/nat/dnf.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+DNF transformation.
+-/
 
-DNF transformation. -/
 import tactic.omega.clause
 import tactic.omega.nat.form
 
diff --git a/src/tactic/omega/nat/form.lean b/src/tactic/omega/nat/form.lean
index 54e48c3720628..2c9899c5bdb2d 100644
--- a/src/tactic/omega/nat/form.lean
+++ b/src/tactic/omega/nat/form.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+Linear natural number arithmetic preformulas in pre-normalized preform.
+-/
 
-Linear natural number arithmetic preformulas in pre-normalized preform. -/
 import tactic.omega.nat.preterm
 
 namespace omega
diff --git a/src/tactic/omega/nat/main.lean b/src/tactic/omega/nat/main.lean
index f006f1385f307..f57f8e34e62db 100644
--- a/src/tactic/omega/nat/main.lean
+++ b/src/tactic/omega/nat/main.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+Main procedure for linear natural number arithmetic.
+-/
 
-Main procedure for linear natural number arithmetic. -/
 import tactic.omega.prove_unsats
 import tactic.omega.nat.dnf
 import tactic.omega.nat.neg_elim
diff --git a/src/tactic/omega/nat/neg_elim.lean b/src/tactic/omega/nat/neg_elim.lean
index 56825206d10d7..10923aeb46169 100644
--- a/src/tactic/omega/nat/neg_elim.lean
+++ b/src/tactic/omega/nat/neg_elim.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+Negation elimination.
+-/
 
-Negation elimination. -/
 import tactic.omega.nat.form
 
 namespace omega
diff --git a/src/tactic/omega/nat/preterm.lean b/src/tactic/omega/nat/preterm.lean
index 2e9e4371d7485..b05bc0c7b163d 100644
--- a/src/tactic/omega/nat/preterm.lean
+++ b/src/tactic/omega/nat/preterm.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+Linear natural number arithmetic terms in pre-normalized form.
+-/
 
-Linear natural number arithmetic terms in pre-normalized form. -/
 import tactic.omega.term
 
 open tactic
diff --git a/src/tactic/omega/nat/sub_elim.lean b/src/tactic/omega/nat/sub_elim.lean
index c487e5ee8041c..dd0aaf75059c2 100644
--- a/src/tactic/omega/nat/sub_elim.lean
+++ b/src/tactic/omega/nat/sub_elim.lean
@@ -1,10 +1,15 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
 
+/-
 Subtraction elimination for linear natural number arithmetic.
 Works by repeatedly rewriting goals of the preform `P[t-s]` into
-`P[x] ∧ (t = s + x ∨ (t ≤ s ∧ x = 0))`, where `x` is fresh. -/
+`P[x] ∧ (t = s + x ∨ (t ≤ s ∧ x = 0))`, where `x` is fresh.
+-/
+
 import tactic.omega.nat.form
 
 namespace omega
diff --git a/src/tactic/omega/prove_unsats.lean b/src/tactic/omega/prove_unsats.lean
index 45708ce72e434..7f0530263b7cd 100644
--- a/src/tactic/omega/prove_unsats.lean
+++ b/src/tactic/omega/prove_unsats.lean
@@ -1,9 +1,14 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
 
+/-
 A tactic which constructs exprs to discharge
-goals of the form `clauses.unsat cs`. -/
+goals of the form `clauses.unsat cs`.
+-/
+
 import tactic.omega.find_ees
 import tactic.omega.find_scalars
 import tactic.omega.lin_comb
diff --git a/src/tactic/omega/term.lean b/src/tactic/omega/term.lean
index 7e79f969715a5..40f6f5b4cdc48 100644
--- a/src/tactic/omega/term.lean
+++ b/src/tactic/omega/term.lean
@@ -1,8 +1,13 @@
-/- Copyright (c) 2019 Seul Baek. All rights reserved.
+/-
+Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
+-/
+
+/-
+Normalized linear integer arithmetic terms.
+-/
 
-Normalized linear integer arithmetic terms. -/
 import tactic.omega.coeffs
 
 namespace omega