Merge pull request #2102 from jdchristensen/emacs-headers

Remove emacs headers and put visual-line-mode in .dir-locals.el

.dir-locals.el

@@ -0,0 +1 @@
+((nil . ((mode . visual-line))))

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

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. *)

theories/Algebra/Aut.v

@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import Basics.
 Require Import Truncations.
 Require Import Algebra.ooGroup.

theories/Algebra/ooAction.v

@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 Require Import Basics.
 Require Import Algebra.ooGroup.
 

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.

theories/Basics/Contractible.v

@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Contractibility *)
 
 Require Import Overture PathGroupoids.

theories/Basics/Decidable.v

@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import
   Basics.Overture
   Basics.PathGroupoids

theories/Basics/Equivalences.v

@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 (** * Equivalences *)
 
 Require Import

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. *)

theories/Basics/PathGroupoids.v

@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 (** * The groupid structure of paths *)
 
 Require Import Basics.Overture Basics.Tactics.

theories/Basics/Trunc.v

@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 (** * Truncatedness *)
 
 Require Import

theories/Colimits/MappingCylinder.v

@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Mapping Cylinders *)
 
 Require Import HoTT.Basics Cubical.DPath Cubical.PathSquare.

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.

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.

theories/Equiv/BiInv.v

@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 Require Import HoTT.Basics HoTT.Types.
 
 Local Open Scope path_scope.

theories/Equiv/PathSplit.v

@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 Require Import HoTT.Basics HoTT.Types.
 
 Local Open Scope nat_scope.

theories/Equiv/Relational.v

@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 Require Import HoTT.Basics HoTT.Types.
 
 Local Open Scope nat_scope.

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.

theories/Extensions.v

@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Extensions and extendible maps *)
 
 Require Import HoTT.Basics HoTT.Types.

theories/Factorization.v

@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Factorizations and factorization systems. *)
 
 Require Import HoTT.Basics HoTT.Types.

theories/HFiber.v

@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics Types Diagrams.CommutativeSquares HSet.
 
 Local Open Scope equiv_scope.

theories/HIT/Flattening.v

@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * The flattening lemma. *)
 
 Require Import HoTT.Basics.

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.

theories/HIT/Interval.v

@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Theorems about the homotopical interval. *)
 
 Require Import Basics.Overture Basics.PathGroupoids.

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.

theories/HIT/V.v

@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * The cumulative hierarchy [V]. *)
 
 Require Import HoTT.Basics HoTT.Types.

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.

theories/Homotopy/ExactSequence.v

@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import Basics Types.
 Require Import SuccessorStructure.
 Require Import WildCat.

theories/Homotopy/Suspension.v

@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics.
 Require Import Types.
 Require Import Cubical.

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.

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.

theories/Metatheory/Core.v

@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 Require Import HoTT.Basics HoTT.Types.
 
 (** * Metatheory *)

theories/Metatheory/FunextVarieties.v

@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Varieties of function extensionality *)
 
 Require Import HoTT.Basics HoTT.Types.

theories/Metatheory/ImpredicativeTruncation.v

@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 (** * Impredicative truncations. *)
 
 Require Import HoTT.Basics.

theories/Metatheory/IntervalImpliesFunext.v

@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Theorems about the homotopical interval. *)
 
 Require Import HoTT.Basics.

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.

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.

theories/Metatheory/UnivalenceVarieties.v

@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 (** * Varieties of univalence *)
 
 Require Import HoTT.Basics HoTT.Types.

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:

theories/Modalities/Accessible.v

@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Accessible subuniverses and modalities *)
 
 Require Import HoTT.Basics HoTT.Types.

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.

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.
 

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.

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.

theories/Modalities/Identity.v

@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Modality Accessible.
 

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.

theories/Modalities/Localization.v

@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 (** * Localization *)
 
 Require Import HoTT.Basics HoTT.Types.

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.

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. *)

theories/Modalities/Notnot.v

@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Modality.
 

theories/Modalities/Nullification.v

@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 (** * Nullification *)
 
 Require Import HoTT.Basics HoTT.Types.

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.

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.

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.

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.

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.

theories/Pointed/Core.v

@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics Types.
 Require Import PathAny.
 Require Import WildCat.

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.

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.

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.

theories/Spaces/Cantor.v

@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 
 Local Open Scope nat_scope.

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.

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.

theories/Spaces/Finite/Fin.v

@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics.
 Require Import Types.
 Require Import HSet.

theories/Spaces/Finite/Finite.v

@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics.
 Require Import Types.
 Require Import HSet.

theories/Spaces/Finite/Tactics.v

@@ -1,4 +1,3 @@
-
 Require Import HoTT.Basics Fin.
 
 (** ** Tactics *)

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.
 

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.

theories/Spaces/No/Negation.v

@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics.
 Require Import HoTT.Spaces.No.Core.
 

theories/Spaces/Spheres.v

@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics Types.
 Require Import WildCat.Equiv.
 Require Import NullHomotopy.

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.

theories/Spectra/Spectrum.v

@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Spectra *)
 
 Require Import HoTT.Basics HoTT.Types.

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.