From 61ef250560d68f90fdbaddec46ceb677ab2226e6 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Wed, 25 Sep 2024 20:27:44 -0400
Subject: [PATCH] Remove emacs headers and put visual-line-mode in
 .dir-locals.el

---
 .dir-locals.el                                   | 1 +
 STYLE.md                                         | 6 +++---
 contrib/SetoidRewrite.v                          | 2 --
 theories/Algebra/Aut.v                           | 1 -
 theories/Algebra/ooAction.v                      | 2 --
 theories/Algebra/ooGroup.v                       | 1 -
 theories/Basics/Contractible.v                   | 2 --
 theories/Basics/Decidable.v                      | 1 -
 theories/Basics/Equivalences.v                   | 1 -
 theories/Basics/Overture.v                       | 2 --
 theories/Basics/PathGroupoids.v                  | 2 --
 theories/Basics/Trunc.v                          | 2 --
 theories/Colimits/MappingCylinder.v              | 2 --
 theories/Colimits/Pushout.v                      | 1 -
 theories/Constant.v                              | 1 -
 theories/Equiv/BiInv.v                           | 2 --
 theories/Equiv/PathSplit.v                       | 2 --
 theories/Equiv/Relational.v                      | 2 --
 theories/EquivGroupoids.v                        | 2 --
 theories/Extensions.v                            | 2 --
 theories/Factorization.v                         | 2 --
 theories/HFiber.v                                | 1 -
 theories/HIT/Flattening.v                        | 2 --
 theories/HIT/FreeIntQuotient.v                   | 1 -
 theories/HIT/Interval.v                          | 2 --
 theories/HIT/SetCone.v                           | 1 -
 theories/HIT/V.v                                 | 2 --
 theories/HIT/quotient.v                          | 1 -
 theories/Homotopy/ExactSequence.v                | 1 -
 theories/Homotopy/Suspension.v                   | 1 -
 theories/Idempotents.v                           | 1 -
 theories/Limits/Pullback.v                       | 1 -
 theories/Metatheory/Core.v                       | 2 --
 theories/Metatheory/FunextVarieties.v            | 2 --
 theories/Metatheory/ImpredicativeTruncation.v    | 1 -
 theories/Metatheory/IntervalImpliesFunext.v      | 2 --
 theories/Metatheory/Nat.v                        | 1 -
 theories/Metatheory/TruncImpliesFunext.v         | 2 --
 theories/Metatheory/UnivalenceVarieties.v        | 1 -
 theories/Misc.v                                  | 1 -
 theories/Modalities/Accessible.v                 | 2 --
 theories/Modalities/Closed.v                     | 2 --
 theories/Modalities/CoreflectiveSubuniverse.v    | 1 -
 theories/Modalities/Descent.v                    | 1 -
 theories/Modalities/Fracture.v                   | 1 -
 theories/Modalities/Identity.v                   | 1 -
 theories/Modalities/Lex.v                        | 1 -
 theories/Modalities/Localization.v               | 1 -
 theories/Modalities/Meet.v                       | 1 -
 theories/Modalities/Modality.v                   | 1 -
 theories/Modalities/Notnot.v                     | 1 -
 theories/Modalities/Nullification.v              | 1 -
 theories/Modalities/Open.v                       | 2 --
 theories/Modalities/ReflectiveSubuniverse.v      | 1 -
 theories/Modalities/Separated.v                  | 1 -
 theories/Modalities/Topological.v                | 1 -
 theories/NullHomotopy.v                          | 1 -
 theories/Pointed/Core.v                          | 1 -
 theories/Spaces/BAut/Bool.v                      | 1 -
 theories/Spaces/BAut/Bool/IncoherentIdempotent.v | 1 -
 theories/Spaces/BAut/Cantor.v                    | 1 -
 theories/Spaces/Cantor.v                         | 1 -
 theories/Spaces/Card.v                           | 1 -
 theories/Spaces/Circle.v                         | 1 -
 theories/Spaces/Finite/Fin.v                     | 1 -
 theories/Spaces/Finite/Finite.v                  | 1 -
 theories/Spaces/Finite/Tactics.v                 | 1 -
 theories/Spaces/No/Addition.v                    | 1 -
 theories/Spaces/No/Core.v                        | 1 -
 theories/Spaces/No/Negation.v                    | 1 -
 theories/Spaces/Spheres.v                        | 1 -
 theories/Spaces/TwoSphere.v                      | 1 -
 theories/Spectra/Spectrum.v                      | 2 --
 theories/Tactics.v                               | 2 --
 theories/Tactics/BinderApply.v                   | 2 --
 theories/Tactics/EvalIn.v                        | 2 --
 theories/Truncations/Connectedness.v             | 1 -
 theories/Truncations/Core.v                      | 2 --
 theories/Truncations/SeparatedTrunc.v            | 2 --
 theories/Types/Arrow.v                           | 1 -
 theories/Types/Bool.v                            | 1 -
 theories/Types/Empty.v                           | 1 -
 theories/Types/Equiv.v                           | 2 --
 theories/Types/Forall.v                          | 1 -
 theories/Types/Paths.v                           | 1 -
 theories/Types/Prod.v                            | 1 -
 theories/Types/Sigma.v                           | 2 --
 theories/Types/Sum.v                             | 1 -
 theories/Types/Unit.v                            | 1 -
 theories/Types/Universe.v                        | 2 --
 theories/Types/WType.v                           | 1 -
 theories/Universes/Automorphisms.v               | 1 -
 theories/Universes/BAut.v                        | 1 -
 theories/Universes/DProp.v                       | 2 --
 theories/Universes/HProp.v                       | 1 -
 theories/Universes/HSet.v                        | 1 -
 theories/Universes/Rigid.v                       | 1 -
 theories/Universes/TruncType.v                   | 1 -
 theories/WildCat/Core.v                          | 2 --
 theories/WildCat/Equiv.v                         | 2 --
 theories/WildCat/EquivGpd.v                      | 2 --
 theories/WildCat/Forall.v                        | 2 --
 theories/WildCat/FunctorCat.v                    | 2 --
 theories/WildCat/Induced.v                       | 2 --
 theories/WildCat/Opposite.v                      | 2 --
 theories/WildCat/Prod.v                          | 2 --
 theories/WildCat/Sigma.v                         | 2 --
 theories/WildCat/Sum.v                           | 2 --
 theories/WildCat/Yoneda.v                        | 2 --
 109 files changed, 4 insertions(+), 154 deletions(-)
 create mode 100644 .dir-locals.el

diff --git a/.dir-locals.el b/.dir-locals.el
new file mode 100644
index 00000000000..f649a9e6b58
--- /dev/null
+++ b/.dir-locals.el
@@ -0,0 +1 @@
+((nil . ((mode . visual-line))))
diff --git a/STYLE.md b/STYLE.md
index 0e55a2887e7..19380817da4 100644
--- a/STYLE.md
+++ b/STYLE.md
@@ -1025,9 +1025,9 @@ window that is narrower than the width to which you filled it.  If
 editing in Emacs, turn off `auto-fill-mode` and turn on
 `visual-line-mode`; then you'll be able to read comment paragraphs
 without scrolling horizontally, no matter how narrow your window is.
-Some files contain `(* -*- mode: coq; mode: visual-line -*- *)` at the
-top, which does this automatically; feel free to add it to files that
-are missing it.
+The repository contains a file .dir-locals.el in the top-level directory
+which turns on `visual-line-mode` when emacs visits any file in the
+repository.
 
 Unfortunately, when viewing source code on Github, these long comment
 lines are not wrapped, making them hard to read.  If you use the
diff --git a/contrib/SetoidRewrite.v b/contrib/SetoidRewrite.v
index fe6b38943d9..917569afe6b 100644
--- a/contrib/SetoidRewrite.v
+++ b/contrib/SetoidRewrite.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 (* Typeclass instances to allow rewriting in categories. Examples are given later in the file. *)
 
 (* Init.Tactics contains the definition of the Coq stdlib typeclass_inferences database. It must be imported before Basics.Overture. *)
diff --git a/theories/Algebra/Aut.v b/theories/Algebra/Aut.v
index b4c26775916..5a59bf283d0 100644
--- a/theories/Algebra/Aut.v
+++ b/theories/Algebra/Aut.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import Basics.
 Require Import Truncations.
 Require Import Algebra.ooGroup.
diff --git a/theories/Algebra/ooAction.v b/theories/Algebra/ooAction.v
index 316483c1434..6ac11c44629 100644
--- a/theories/Algebra/ooAction.v
+++ b/theories/Algebra/ooAction.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 Require Import Basics.
 Require Import Algebra.ooGroup.
 
diff --git a/theories/Algebra/ooGroup.v b/theories/Algebra/ooGroup.v
index 7d0f6b87d85..6192c216a78 100644
--- a/theories/Algebra/ooGroup.v
+++ b/theories/Algebra/ooGroup.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import Basics Types.
 Require Import Pointed.
 Require Import Truncations.Core Truncations.Connectedness.
diff --git a/theories/Basics/Contractible.v b/theories/Basics/Contractible.v
index f77f8ea0b4d..c74533067f2 100644
--- a/theories/Basics/Contractible.v
+++ b/theories/Basics/Contractible.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Contractibility *)
 
 Require Import Overture PathGroupoids.
diff --git a/theories/Basics/Decidable.v b/theories/Basics/Decidable.v
index 2f7614351f3..85b875a6d9b 100644
--- a/theories/Basics/Decidable.v
+++ b/theories/Basics/Decidable.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import
   Basics.Overture
   Basics.PathGroupoids
diff --git a/theories/Basics/Equivalences.v b/theories/Basics/Equivalences.v
index 9384495d478..03e407780a7 100644
--- a/theories/Basics/Equivalences.v
+++ b/theories/Basics/Equivalences.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 (** * Equivalences *)
 
 Require Import
diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v
index 31902f2d23e..1d894e7ebf0 100644
--- a/theories/Basics/Overture.v
+++ b/theories/Basics/Overture.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 (** * Basic definitions of homotopy type theory *)
 
 (** This file defines some of the most basic types and type formers, such as sums, products, Sigma types and path types.  It defines the action of functions on paths [ap], transport, equivalences, and function extensionality.  It also defines truncatedness, and a number of other fundamental definitions used throughout the library. *)
diff --git a/theories/Basics/PathGroupoids.v b/theories/Basics/PathGroupoids.v
index 2b7bc99b93c..d7cd4e9fde3 100644
--- a/theories/Basics/PathGroupoids.v
+++ b/theories/Basics/PathGroupoids.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 (** * The groupid structure of paths *)
 
 Require Import Basics.Overture Basics.Tactics.
diff --git a/theories/Basics/Trunc.v b/theories/Basics/Trunc.v
index 0fc8d472b86..2eea8499827 100644
--- a/theories/Basics/Trunc.v
+++ b/theories/Basics/Trunc.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 (** * Truncatedness *)
 
 Require Import
diff --git a/theories/Colimits/MappingCylinder.v b/theories/Colimits/MappingCylinder.v
index 1e7ae14eb7a..91ecda6e1ec 100644
--- a/theories/Colimits/MappingCylinder.v
+++ b/theories/Colimits/MappingCylinder.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Mapping Cylinders *)
 
 Require Import HoTT.Basics Cubical.DPath Cubical.PathSquare.
diff --git a/theories/Colimits/Pushout.v b/theories/Colimits/Pushout.v
index 3273310c877..a61159d373c 100644
--- a/theories/Colimits/Pushout.v
+++ b/theories/Colimits/Pushout.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics.
 Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.
 Require Export Colimits.Coeq.
diff --git a/theories/Constant.v b/theories/Constant.v
index 146e8b8325a..c830cbd9cbe 100644
--- a/theories/Constant.v
+++ b/theories/Constant.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Extensions Factorization.
 Require Import Truncations.Core Modalities.Modality.
diff --git a/theories/Equiv/BiInv.v b/theories/Equiv/BiInv.v
index 3861cbfe5c9..c58bbf44e95 100644
--- a/theories/Equiv/BiInv.v
+++ b/theories/Equiv/BiInv.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 Require Import HoTT.Basics HoTT.Types.
 
 Local Open Scope path_scope.
diff --git a/theories/Equiv/PathSplit.v b/theories/Equiv/PathSplit.v
index b861351f7bd..24b966a04fc 100644
--- a/theories/Equiv/PathSplit.v
+++ b/theories/Equiv/PathSplit.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 Require Import HoTT.Basics HoTT.Types.
 
 Local Open Scope nat_scope.
diff --git a/theories/Equiv/Relational.v b/theories/Equiv/Relational.v
index b5c75cec50b..621881b2348 100644
--- a/theories/Equiv/Relational.v
+++ b/theories/Equiv/Relational.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 Require Import HoTT.Basics HoTT.Types.
 
 Local Open Scope nat_scope.
diff --git a/theories/EquivGroupoids.v b/theories/EquivGroupoids.v
index 184836fe568..0a6ef53db69 100644
--- a/theories/EquivGroupoids.v
+++ b/theories/EquivGroupoids.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 (** * The pregroupoid structure of [Equiv] *)
 
 Require Import Basics.Overture Basics.Equivalences Types.Equiv.
diff --git a/theories/Extensions.v b/theories/Extensions.v
index bacb14cba98..7ea763df37b 100644
--- a/theories/Extensions.v
+++ b/theories/Extensions.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Extensions and extendible maps *)
 
 Require Import HoTT.Basics HoTT.Types.
diff --git a/theories/Factorization.v b/theories/Factorization.v
index e407a64582e..a9fbd3f8084 100644
--- a/theories/Factorization.v
+++ b/theories/Factorization.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Factorizations and factorization systems. *)
 
 Require Import HoTT.Basics HoTT.Types.
diff --git a/theories/HFiber.v b/theories/HFiber.v
index d5f4267a7ca..0c914278e71 100644
--- a/theories/HFiber.v
+++ b/theories/HFiber.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics Types Diagrams.CommutativeSquares HSet.
 
 Local Open Scope equiv_scope.
diff --git a/theories/HIT/Flattening.v b/theories/HIT/Flattening.v
index d9f41a8afe4..8b9d5f39d46 100644
--- a/theories/HIT/Flattening.v
+++ b/theories/HIT/Flattening.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * The flattening lemma. *)
 
 Require Import HoTT.Basics.
diff --git a/theories/HIT/FreeIntQuotient.v b/theories/HIT/FreeIntQuotient.v
index f80293dc40b..1d575056518 100644
--- a/theories/HIT/FreeIntQuotient.v
+++ b/theories/HIT/FreeIntQuotient.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Spaces.Int Spaces.Circle.
 Require Import Colimits.Coeq HIT.Flattening Truncations.Core Truncations.Connectedness.
diff --git a/theories/HIT/Interval.v b/theories/HIT/Interval.v
index 195e1c66675..b3dbcd20560 100644
--- a/theories/HIT/Interval.v
+++ b/theories/HIT/Interval.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Theorems about the homotopical interval. *)
 
 Require Import Basics.Overture Basics.PathGroupoids.
diff --git a/theories/HIT/SetCone.v b/theories/HIT/SetCone.v
index 5c787a7fe69..c98a5d3f852 100644
--- a/theories/HIT/SetCone.v
+++ b/theories/HIT/SetCone.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics Types.Unit.
 Require Import Colimits.Pushout.
 Require Import Truncations.Core.
diff --git a/theories/HIT/V.v b/theories/HIT/V.v
index 3edc673424e..6853e7c48b1 100644
--- a/theories/HIT/V.v
+++ b/theories/HIT/V.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * The cumulative hierarchy [V]. *)
 
 Require Import HoTT.Basics HoTT.Types.
diff --git a/theories/HIT/quotient.v b/theories/HIT/quotient.v
index 428e05ffc50..525e4e32762 100644
--- a/theories/HIT/quotient.v
+++ b/theories/HIT/quotient.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import HSet TruncType.
 Require Import Truncations.Core.
diff --git a/theories/Homotopy/ExactSequence.v b/theories/Homotopy/ExactSequence.v
index c42fcae4485..3c379e92745 100644
--- a/theories/Homotopy/ExactSequence.v
+++ b/theories/Homotopy/ExactSequence.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import Basics Types.
 Require Import SuccessorStructure.
 Require Import WildCat.
diff --git a/theories/Homotopy/Suspension.v b/theories/Homotopy/Suspension.v
index b3173ed52c2..ff0c308f4c6 100644
--- a/theories/Homotopy/Suspension.v
+++ b/theories/Homotopy/Suspension.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics.
 Require Import Types.
 Require Import Cubical.
diff --git a/theories/Idempotents.v b/theories/Idempotents.v
index ce2115bc672..6ca808b90c2 100644
--- a/theories/Idempotents.v
+++ b/theories/Idempotents.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import HFiber Constant.
 Require Import Truncations.Core Modalities.Modality.
diff --git a/theories/Limits/Pullback.v b/theories/Limits/Pullback.v
index d0e90b25233..26f2c63ab2a 100644
--- a/theories/Limits/Pullback.v
+++ b/theories/Limits/Pullback.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import HFiber PathAny Cubical.PathSquare.
 Require Import Diagrams.CommutativeSquares.
diff --git a/theories/Metatheory/Core.v b/theories/Metatheory/Core.v
index 9916146588d..cc6a37d0dc1 100644
--- a/theories/Metatheory/Core.v
+++ b/theories/Metatheory/Core.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 Require Import HoTT.Basics HoTT.Types.
 
 (** * Metatheory *)
diff --git a/theories/Metatheory/FunextVarieties.v b/theories/Metatheory/FunextVarieties.v
index f3caa108cd2..399da75a3a5 100644
--- a/theories/Metatheory/FunextVarieties.v
+++ b/theories/Metatheory/FunextVarieties.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Varieties of function extensionality *)
 
 Require Import HoTT.Basics HoTT.Types.
diff --git a/theories/Metatheory/ImpredicativeTruncation.v b/theories/Metatheory/ImpredicativeTruncation.v
index 352a87247a2..8920f479719 100644
--- a/theories/Metatheory/ImpredicativeTruncation.v
+++ b/theories/Metatheory/ImpredicativeTruncation.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 (** * Impredicative truncations. *)
 
 Require Import HoTT.Basics.
diff --git a/theories/Metatheory/IntervalImpliesFunext.v b/theories/Metatheory/IntervalImpliesFunext.v
index fe9d97d48ad..5a43e5593b7 100644
--- a/theories/Metatheory/IntervalImpliesFunext.v
+++ b/theories/Metatheory/IntervalImpliesFunext.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Theorems about the homotopical interval. *)
 
 Require Import HoTT.Basics.
diff --git a/theories/Metatheory/Nat.v b/theories/Metatheory/Nat.v
index ec5bc3993b2..423173bd88a 100644
--- a/theories/Metatheory/Nat.v
+++ b/theories/Metatheory/Nat.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 (** * Defining the natural numbers from univalence and propresizing. *)
 Require Import Basics.
 Require Import Types.
diff --git a/theories/Metatheory/TruncImpliesFunext.v b/theories/Metatheory/TruncImpliesFunext.v
index d697be8198d..c4a0ed409d2 100644
--- a/theories/Metatheory/TruncImpliesFunext.v
+++ b/theories/Metatheory/TruncImpliesFunext.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Theorems about trunctions *)
 
 Require Import HoTT.Basics HoTT.Truncations HoTT.Types.Bool.
diff --git a/theories/Metatheory/UnivalenceVarieties.v b/theories/Metatheory/UnivalenceVarieties.v
index dc0ec9bd423..35342a788d4 100644
--- a/theories/Metatheory/UnivalenceVarieties.v
+++ b/theories/Metatheory/UnivalenceVarieties.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 (** * Varieties of univalence *)
 
 Require Import HoTT.Basics HoTT.Types.
diff --git a/theories/Misc.v b/theories/Misc.v
index 15eeeee16ae..6536189a2be 100644
--- a/theories/Misc.v
+++ b/theories/Misc.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 (** * Miscellaneous material *)
 
 (** If you have a lemma or group of lemmas that you can’t find a better home for, put them here.  However, big “Miscellaneous” files are sub-optimal to work with, so some caveats:
diff --git a/theories/Modalities/Accessible.v b/theories/Modalities/Accessible.v
index 582a358a17f..c4de9deb026 100644
--- a/theories/Modalities/Accessible.v
+++ b/theories/Modalities/Accessible.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Accessible subuniverses and modalities *)
 
 Require Import HoTT.Basics HoTT.Types.
diff --git a/theories/Modalities/Closed.v b/theories/Modalities/Closed.v
index 597eedd8a91..9a55fa7b619 100644
--- a/theories/Modalities/Closed.v
+++ b/theories/Modalities/Closed.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 Require Import HoTT.Basics HoTT.Types.
 Require Import Extensions.
 Require Import Modality Accessible Nullification Lex Topological.
diff --git a/theories/Modalities/CoreflectiveSubuniverse.v b/theories/Modalities/CoreflectiveSubuniverse.v
index 4641e5225ab..15d94de1a86 100644
--- a/theories/Modalities/CoreflectiveSubuniverse.v
+++ b/theories/Modalities/CoreflectiveSubuniverse.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Modalities.Modality Modalities.Open.
 
diff --git a/theories/Modalities/Descent.v b/theories/Modalities/Descent.v
index 2bb68d9cff3..1a26e13eba4 100644
--- a/theories/Modalities/Descent.v
+++ b/theories/Modalities/Descent.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import HFiber Extensions Limits.Pullback.
 Require Import Modality Accessible Modalities.Localization.
diff --git a/theories/Modalities/Fracture.v b/theories/Modalities/Fracture.v
index c9e306bee33..b0773f75939 100644
--- a/theories/Modalities/Fracture.v
+++ b/theories/Modalities/Fracture.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Extensions Limits.Pullback.
 Require Import Modality Lex Open Closed Nullification.
diff --git a/theories/Modalities/Identity.v b/theories/Modalities/Identity.v
index 067a2360d69..3bd81e73bbb 100644
--- a/theories/Modalities/Identity.v
+++ b/theories/Modalities/Identity.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Modality Accessible.
 
diff --git a/theories/Modalities/Lex.v b/theories/Modalities/Lex.v
index 68c0c725d55..ab5e35380d6 100644
--- a/theories/Modalities/Lex.v
+++ b/theories/Modalities/Lex.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import HFiber Limits.Pullback Factorization Truncations.Core.
 Require Import Modality Accessible Modalities.Localization Descent Separated.
diff --git a/theories/Modalities/Localization.v b/theories/Modalities/Localization.v
index ee7edc0f1a8..46d8e5e4804 100644
--- a/theories/Modalities/Localization.v
+++ b/theories/Modalities/Localization.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 (** * Localization *)
 
 Require Import HoTT.Basics HoTT.Types.
diff --git a/theories/Modalities/Meet.v b/theories/Modalities/Meet.v
index 96ad8d18d1a..ac684fbb339 100644
--- a/theories/Modalities/Meet.v
+++ b/theories/Modalities/Meet.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Extensions HFiber Truncations NullHomotopy Limits.Pullback.
 Require Import Descent Lex Separated.
diff --git a/theories/Modalities/Modality.v b/theories/Modalities/Modality.v
index fa74bf88bc1..a1abf512b16 100644
--- a/theories/Modalities/Modality.v
+++ b/theories/Modalities/Modality.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import HFiber Extensions Factorization Limits.Pullback.
 Require Export ReflectiveSubuniverse. (* [Export] because many of the lemmas and facts about reflective subuniverses are equally important for modalities. *)
diff --git a/theories/Modalities/Notnot.v b/theories/Modalities/Notnot.v
index d2f2d93c43a..eb67954c0a8 100644
--- a/theories/Modalities/Notnot.v
+++ b/theories/Modalities/Notnot.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Modality.
 
diff --git a/theories/Modalities/Nullification.v b/theories/Modalities/Nullification.v
index ac6dda799fc..8c19bd0a24a 100644
--- a/theories/Modalities/Nullification.v
+++ b/theories/Modalities/Nullification.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 (** * Nullification *)
 
 Require Import HoTT.Basics HoTT.Types.
diff --git a/theories/Modalities/Open.v b/theories/Modalities/Open.v
index 6c556c4df6a..851c1e5ff6f 100644
--- a/theories/Modalities/Open.v
+++ b/theories/Modalities/Open.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 Require Import HoTT.Basics HoTT.Types.
 Require Import Extensions.
 Require Import Modality Accessible Nullification Lex.
diff --git a/theories/Modalities/ReflectiveSubuniverse.v b/theories/Modalities/ReflectiveSubuniverse.v
index 72480c5ea88..1bef8b18c87 100644
--- a/theories/Modalities/ReflectiveSubuniverse.v
+++ b/theories/Modalities/ReflectiveSubuniverse.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback.
 Require Import PathAny.
diff --git a/theories/Modalities/Separated.v b/theories/Modalities/Separated.v
index c27a421bd78..451f556d860 100644
--- a/theories/Modalities/Separated.v
+++ b/theories/Modalities/Separated.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import HoTT.Basics HoTT.Types HoTT.Cubical.DPath.
 Require Import HFiber Extensions Factorization Limits.Pullback.
 Require Import Modality Accessible Descent.
diff --git a/theories/Modalities/Topological.v b/theories/Modalities/Topological.v
index 0a1c7420bfa..3f511571e2f 100644
--- a/theories/Modalities/Topological.v
+++ b/theories/Modalities/Topological.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Extensions HoTT.Truncations.
 Require Import Accessible Lex Nullification.
diff --git a/theories/NullHomotopy.v b/theories/NullHomotopy.v
index f6e9a4ecace..b572920bbab 100644
--- a/theories/NullHomotopy.v
+++ b/theories/NullHomotopy.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics.
 Require Import Types.Sigma.
 Local Open Scope path_scope.
diff --git a/theories/Pointed/Core.v b/theories/Pointed/Core.v
index ec69938b3b9..bb212207296 100644
--- a/theories/Pointed/Core.v
+++ b/theories/Pointed/Core.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics Types.
 Require Import PathAny.
 Require Import WildCat.
diff --git a/theories/Spaces/BAut/Bool.v b/theories/Spaces/BAut/Bool.v
index 02c13e90a18..1feea506d5e 100644
--- a/theories/Spaces/BAut/Bool.v
+++ b/theories/Spaces/BAut/Bool.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Constant.
 Require Import HoTT.Truncations.Core HoTT.Truncations.Connectedness.
diff --git a/theories/Spaces/BAut/Bool/IncoherentIdempotent.v b/theories/Spaces/BAut/Bool/IncoherentIdempotent.v
index ca6315cfcce..1445931a6e9 100644
--- a/theories/Spaces/BAut/Bool/IncoherentIdempotent.v
+++ b/theories/Spaces/BAut/Bool/IncoherentIdempotent.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Equiv.BiInv Idempotents.
 Require Import Universes.BAut Spaces.BAut.Bool.
diff --git a/theories/Spaces/BAut/Cantor.v b/theories/Spaces/BAut/Cantor.v
index be8465b3cb3..307b9b403ad 100644
--- a/theories/Spaces/BAut/Cantor.v
+++ b/theories/Spaces/BAut/Cantor.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Idempotents.
 Require Import HoTT.Truncations.Core Universes.BAut Spaces.Cantor.
diff --git a/theories/Spaces/Cantor.v b/theories/Spaces/Cantor.v
index a54132cfcd5..d30b9704d25 100644
--- a/theories/Spaces/Cantor.v
+++ b/theories/Spaces/Cantor.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 
 Local Open Scope nat_scope.
diff --git a/theories/Spaces/Card.v b/theories/Spaces/Card.v
index e07b27311c3..95fa0f3ea25 100644
--- a/theories/Spaces/Card.v
+++ b/theories/Spaces/Card.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 (** Representation of cardinals, see Chapter 10 of the HoTT book. *)
 Require Import HoTT.Universes.TruncType.
 Require Import HoTT.Classes.interfaces.abstract_algebra.
diff --git a/theories/Spaces/Circle.v b/theories/Spaces/Circle.v
index ba4bf1f75ea..de953c6d984 100644
--- a/theories/Spaces/Circle.v
+++ b/theories/Spaces/Circle.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics Types.
 Require Import Pointed.Core Pointed.Loops Pointed.pEquiv.
 Require Import HSet.
diff --git a/theories/Spaces/Finite/Fin.v b/theories/Spaces/Finite/Fin.v
index afff1f75d04..c3caef63187 100644
--- a/theories/Spaces/Finite/Fin.v
+++ b/theories/Spaces/Finite/Fin.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics.
 Require Import Types.
 Require Import HSet.
diff --git a/theories/Spaces/Finite/Finite.v b/theories/Spaces/Finite/Finite.v
index 648850a28e0..6a686a6dd59 100644
--- a/theories/Spaces/Finite/Finite.v
+++ b/theories/Spaces/Finite/Finite.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics.
 Require Import Types.
 Require Import HSet.
diff --git a/theories/Spaces/Finite/Tactics.v b/theories/Spaces/Finite/Tactics.v
index 326f950587d..5268758258b 100644
--- a/theories/Spaces/Finite/Tactics.v
+++ b/theories/Spaces/Finite/Tactics.v
@@ -1,4 +1,3 @@
-
 Require Import HoTT.Basics Fin.
 
 (** ** Tactics *)
diff --git a/theories/Spaces/No/Addition.v b/theories/Spaces/No/Addition.v
index 94187db35a8..de8ae2742a9 100644
--- a/theories/Spaces/No/Addition.v
+++ b/theories/Spaces/No/Addition.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import HoTT.Spaces.No.Core HoTT.Spaces.No.Negation.
 
diff --git a/theories/Spaces/No/Core.v b/theories/Spaces/No/Core.v
index 17cc723f81a..fc6998dd02d 100644
--- a/theories/Spaces/No/Core.v
+++ b/theories/Spaces/No/Core.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import TruncType HSet.
 Require Import HoTT.Truncations.Core.
diff --git a/theories/Spaces/No/Negation.v b/theories/Spaces/No/Negation.v
index 52f0e9e3eb4..049c7cda57c 100644
--- a/theories/Spaces/No/Negation.v
+++ b/theories/Spaces/No/Negation.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics.
 Require Import HoTT.Spaces.No.Core.
 
diff --git a/theories/Spaces/Spheres.v b/theories/Spaces/Spheres.v
index d1792fa74be..fbf385477bd 100644
--- a/theories/Spaces/Spheres.v
+++ b/theories/Spaces/Spheres.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics Types.
 Require Import WildCat.Equiv.
 Require Import NullHomotopy.
diff --git a/theories/Spaces/TwoSphere.v b/theories/Spaces/TwoSphere.v
index f20b34b9724..4f3077723e3 100644
--- a/theories/Spaces/TwoSphere.v
+++ b/theories/Spaces/TwoSphere.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids.
 
 Local Open Scope path_scope.
diff --git a/theories/Spectra/Spectrum.v b/theories/Spectra/Spectrum.v
index cdfdc929fd1..cbff0bbec81 100644
--- a/theories/Spectra/Spectrum.v
+++ b/theories/Spectra/Spectrum.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Spectra *)
 
 Require Import HoTT.Basics HoTT.Types.
diff --git a/theories/Tactics.v b/theories/Tactics.v
index 0518bd4438c..1a4bd8366c1 100644
--- a/theories/Tactics.v
+++ b/theories/Tactics.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Contractible Basics.Equivalences.
 Require Import Types.Prod Types.Forall.
 Require Export Tactics.BinderApply.
diff --git a/theories/Tactics/BinderApply.v b/theories/Tactics/BinderApply.v
index aad0b2c4282..10eb746af6d 100644
--- a/theories/Tactics/BinderApply.v
+++ b/theories/Tactics/BinderApply.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 (** * Apply a lemma under binders *)
 Require Import Basics.Overture Tactics.EvalIn.
 (** There are some cases where [apply lem] will fail, but [intros; apply lem] will succeed.  The tactic [binder apply] is like [intros; apply lem], but it cleans up after itself by [revert]ing the things it introduced.  The tactic [binder apply lem in H] is to [binder apply lem], as [apply lem in H] is to [apply lem].  Note, however, that the implementation of [binder apply lem in H] is completely different and significantly more complicated. *)
diff --git a/theories/Tactics/EvalIn.v b/theories/Tactics/EvalIn.v
index cb6625ca050..db547d3b546 100644
--- a/theories/Tactics/EvalIn.v
+++ b/theories/Tactics/EvalIn.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 (** * Evaluating tactics on terms *)
 Require Import Basics.Overture Basics.PathGroupoids.
 
diff --git a/theories/Truncations/Connectedness.v b/theories/Truncations/Connectedness.v
index 6d5792c3e96..eec30829117 100644
--- a/theories/Truncations/Connectedness.v
+++ b/theories/Truncations/Connectedness.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 (** * Connectedness *)
 Require Import Basics.
 Require Import Types.
diff --git a/theories/Truncations/Core.v b/theories/Truncations/Core.v
index 9a7a637c6b0..efd08349605 100644
--- a/theories/Truncations/Core.v
+++ b/theories/Truncations/Core.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 Require Import Basics Types WildCat.Core WildCat.Universe.
 Require Import Modalities.Modality.
 (* Users of this file almost always want to be able to write [Tr n] for both a [Modality] and a [ReflectiveSubuniverse], so they want the coercion [modality_to_reflective_subuniverse]: *)
diff --git a/theories/Truncations/SeparatedTrunc.v b/theories/Truncations/SeparatedTrunc.v
index e2741ae71e0..86301f473f9 100644
--- a/theories/Truncations/SeparatedTrunc.v
+++ b/theories/Truncations/SeparatedTrunc.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 Require Import Basics Types.
 Require Import TruncType.
 Require Import Truncations.Core Modalities.Modality Modalities.Descent.
diff --git a/theories/Types/Arrow.v b/theories/Types/Arrow.v
index 2813833a8d3..f624c44f04b 100644
--- a/theories/Types/Arrow.v
+++ b/theories/Types/Arrow.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 (** * Theorems about Non-dependent function types *)
 
 Require Import Basics.Overture Basics.PathGroupoids Basics.Decidable
diff --git a/theories/Types/Bool.v b/theories/Types/Bool.v
index 61419d0fb9b..b27e833f218 100644
--- a/theories/Types/Bool.v
+++ b/theories/Types/Bool.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 (** * Theorems about the booleans *)
 
 Require Import HoTT.Basics.
diff --git a/theories/Types/Empty.v b/theories/Types/Empty.v
index d7862754815..dcbd8d37fcb 100644
--- a/theories/Types/Empty.v
+++ b/theories/Types/Empty.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 (** * Theorems about the empty type *)
 
 Require Import Basics.Overture Basics.Equivalences Basics.Trunc.
diff --git a/theories/Types/Equiv.v b/theories/Types/Equiv.v
index e80968be808..e7f3e616336 100644
--- a/theories/Types/Equiv.v
+++ b/theories/Types/Equiv.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 Require Import HoTT.Basics.
 Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths.
 
diff --git a/theories/Types/Forall.v b/theories/Types/Forall.v
index 8b30a5247ac..4350958f884 100644
--- a/theories/Types/Forall.v
+++ b/theories/Types/Forall.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 (** * Theorems about dependent products *)
 
 Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids
diff --git a/theories/Types/Paths.v b/theories/Types/Paths.v
index 90d150b0f5e..ccc2b72352c 100644
--- a/theories/Types/Paths.v
+++ b/theories/Types/Paths.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 (** * Theorems about path spaces *)
 
 Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.
diff --git a/theories/Types/Prod.v b/theories/Types/Prod.v
index cb406ea19c1..346390fac78 100644
--- a/theories/Types/Prod.v
+++ b/theories/Types/Prod.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 (** * Theorems about cartesian products *)
 
 Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids
diff --git a/theories/Types/Sigma.v b/theories/Types/Sigma.v
index 4604963f476..b4a41f3c128 100644
--- a/theories/Types/Sigma.v
+++ b/theories/Types/Sigma.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Theorems about Sigma-types (dependent sums) *)
 
 Require Import HoTT.Basics.
diff --git a/theories/Types/Sum.v b/theories/Types/Sum.v
index bcb67b10880..d52e600504b 100644
--- a/theories/Types/Sum.v
+++ b/theories/Types/Sum.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 (** * Theorems about disjoint unions *)
 
 Require Import HoTT.Basics.
diff --git a/theories/Types/Unit.v b/theories/Types/Unit.v
index 3ab36cc309c..745b4ded0d7 100644
--- a/theories/Types/Unit.v
+++ b/theories/Types/Unit.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 (** * Theorems about the unit type *)
 
 Require Import Basics.Overture Basics.Equivalences.
diff --git a/theories/Types/Universe.v b/theories/Types/Universe.v
index fd178852b44..d26b8166e40 100644
--- a/theories/Types/Universe.v
+++ b/theories/Types/Universe.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Theorems about the universe, including the Univalence Axiom. *)
 
 Require Import HoTT.Basics.
diff --git a/theories/Types/WType.v b/theories/Types/WType.v
index 3c9b96c7a0a..7cb658e3a26 100644
--- a/theories/Types/WType.v
+++ b/theories/Types/WType.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics.
 Require Import Types.Forall Types.Sigma.
 
diff --git a/theories/Universes/Automorphisms.v b/theories/Universes/Automorphisms.v
index 96b0f583893..8677134b906 100644
--- a/theories/Universes/Automorphisms.v
+++ b/theories/Universes/Automorphisms.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import Basics Types.
 Require Import HoTT.Truncations.
 Require Import Universes.BAut Universes.Rigid.
diff --git a/theories/Universes/BAut.v b/theories/Universes/BAut.v
index 1cddc92768d..8930d97af54 100644
--- a/theories/Universes/BAut.v
+++ b/theories/Universes/BAut.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Constant.
 Require Import HoTT.Truncations.
diff --git a/theories/Universes/DProp.v b/theories/Universes/DProp.v
index 09f66f622d5..96a10900568 100644
--- a/theories/Universes/DProp.v
+++ b/theories/Universes/DProp.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 (** * Decidable propositions *)
 
 Require Import HoTT.Basics HoTT.Types.
diff --git a/theories/Universes/HProp.v b/theories/Universes/HProp.v
index b9070a95b13..3f014d3161c 100644
--- a/theories/Universes/HProp.v
+++ b/theories/Universes/HProp.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 (** * HPropositions *)
 
 Require Import HoTT.Basics HoTT.Types.
diff --git a/theories/Universes/HSet.v b/theories/Universes/HSet.v
index def22d820ab..00d67d1e06d 100644
--- a/theories/Universes/HSet.v
+++ b/theories/Universes/HSet.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import Basics.
 Require Import Types.Sigma Types.Paths Types.Unit Types.Arrow.
 
diff --git a/theories/Universes/Rigid.v b/theories/Universes/Rigid.v
index d7081fafbdc..86a7830297c 100644
--- a/theories/Universes/Rigid.v
+++ b/theories/Universes/Rigid.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import HFiber.
 Require Import Truncations.
diff --git a/theories/Universes/TruncType.v b/theories/Universes/TruncType.v
index 4a273775d18..de1268063b4 100644
--- a/theories/Universes/TruncType.v
+++ b/theories/Universes/TruncType.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import HProp.
 
diff --git a/theories/WildCat/Core.v b/theories/WildCat/Core.v
index bf917a67d9c..4548ad6c731 100644
--- a/theories/WildCat/Core.v
+++ b/theories/WildCat/Core.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 Require Import Basics.Overture Basics.Tactics.
 
 (** * Wild categories, functors, and transformations *)
diff --git a/theories/WildCat/Equiv.v b/theories/WildCat/Equiv.v
index 240906b2966..c58d8b8be5f 100644
--- a/theories/WildCat/Equiv.v
+++ b/theories/WildCat/Equiv.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences.
 Require Import WildCat.Core.
 Require Import WildCat.Opposite.
diff --git a/theories/WildCat/EquivGpd.v b/theories/WildCat/EquivGpd.v
index a9bda05d356..35bad591164 100644
--- a/theories/WildCat/EquivGpd.v
+++ b/theories/WildCat/EquivGpd.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 Require Import Basics.Overture Basics.Tactics Basics.Iff.
 Require Import WildCat.Core.
 Require Import WildCat.NatTrans.
diff --git a/theories/WildCat/Forall.v b/theories/WildCat/Forall.v
index 25a76f84eb2..025913ba8e4 100644
--- a/theories/WildCat/Forall.v
+++ b/theories/WildCat/Forall.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 Require Import Basics.Overture Basics.Tactics.
 Require Import WildCat.Core.
 
diff --git a/theories/WildCat/FunctorCat.v b/theories/WildCat/FunctorCat.v
index d9c3997a8ac..8cc16d54475 100644
--- a/theories/WildCat/FunctorCat.v
+++ b/theories/WildCat/FunctorCat.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 Require Import Basics.Overture Basics.Tactics.
 Require Import WildCat.Core.
 Require Import WildCat.Opposite.
diff --git a/theories/WildCat/Induced.v b/theories/WildCat/Induced.v
index 0e9dd18c269..279c8a5c2dd 100644
--- a/theories/WildCat/Induced.v
+++ b/theories/WildCat/Induced.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 Require Import Basics.Overture Basics.Tactics.
 Require Import WildCat.Core.
 Require Import WildCat.Equiv.
diff --git a/theories/WildCat/Opposite.v b/theories/WildCat/Opposite.v
index 8d26289d5bf..ec14e546b62 100644
--- a/theories/WildCat/Opposite.v
+++ b/theories/WildCat/Opposite.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 Require Import Basics.Overture Basics.Tactics.
 Require Import WildCat.Core.
 
diff --git a/theories/WildCat/Prod.v b/theories/WildCat/Prod.v
index 12d04db409d..a6d4c5831b6 100644
--- a/theories/WildCat/Prod.v
+++ b/theories/WildCat/Prod.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 Require Import Basics.Overture Basics.Tactics.
 Require Import WildCat.Core.
 Require Import WildCat.Equiv.
diff --git a/theories/WildCat/Sigma.v b/theories/WildCat/Sigma.v
index b0fb96e821b..e39329abb57 100644
--- a/theories/WildCat/Sigma.v
+++ b/theories/WildCat/Sigma.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 Require Import Basics.Overture Basics.Tactics.
 Require Import WildCat.Core.
 
diff --git a/theories/WildCat/Sum.v b/theories/WildCat/Sum.v
index 96564d6ea7f..f17bc72e627 100644
--- a/theories/WildCat/Sum.v
+++ b/theories/WildCat/Sum.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 Require Import Basics.Overture Basics.Tactics.
 Require Import WildCat.Core.
 
diff --git a/theories/WildCat/Yoneda.v b/theories/WildCat/Yoneda.v
index 4af6d842b20..3730aa8517b 100644
--- a/theories/WildCat/Yoneda.v
+++ b/theories/WildCat/Yoneda.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 Require Import Basics.Overture Basics.Tactics.
 Require Import WildCat.Core.
 Require Import WildCat.Equiv.