From 44e3087695aef6e500d2835bab9761176d968309 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Wed, 6 Mar 2024 19:51:28 +0100 Subject: [PATCH] fix end newlines in repo Signed-off-by: Ali Caglayan --- README.md | 2 +- theories/Cubical.v | 2 +- theories/Diagrams/ParallelPair.v | 2 +- theories/Diagrams/Span.v | 2 +- theories/Spaces/Int.v | 2 +- theories/Spaces/Pos.v | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 2e1fb1380f2..0d5deee99db 100644 --- a/README.md +++ b/README.md @@ -99,4 +99,4 @@ More information can be found in the [Wiki][22]. [20]: https://code.visualstudio.com/ [21]: https://github.com/coq-community/vscoq -[22]: https://github.com/HoTT/HoTT/wiki \ No newline at end of file +[22]: https://github.com/HoTT/HoTT/wiki diff --git a/theories/Cubical.v b/theories/Cubical.v index cd1c6d2a455..55ad543a3a3 100644 --- a/theories/Cubical.v +++ b/theories/Cubical.v @@ -2,4 +2,4 @@ Require Export Cubical.DPath. Require Export Cubical.PathSquare. Require Export Cubical.DPathSquare. Require Export Cubical.PathCube. -Require Export Cubical.DPathCube. \ No newline at end of file +Require Export Cubical.DPathCube. diff --git a/theories/Diagrams/ParallelPair.v b/theories/Diagrams/ParallelPair.v index 42838fa0751..2c82ee3456c 100644 --- a/theories/Diagrams/ParallelPair.v +++ b/theories/Diagrams/ParallelPair.v @@ -32,4 +32,4 @@ Proof. srapply Build_Cocone. 1: intros []; [exact (q o f) | exact q]. intros [] [] []; [reflexivity | exact Hq]. -Defined. \ No newline at end of file +Defined. diff --git a/theories/Diagrams/Span.v b/theories/Diagrams/Span.v index c222890451f..db77b436f8b 100644 --- a/theories/Diagrams/Span.v +++ b/theories/Diagrams/Span.v @@ -33,4 +33,4 @@ Section Span. + exact g. Defined. -End Span. \ No newline at end of file +End Span. diff --git a/theories/Spaces/Int.v b/theories/Spaces/Int.v index 2e5c7a9dfee..4587699c4b0 100644 --- a/theories/Spaces/Int.v +++ b/theories/Spaces/Int.v @@ -1,4 +1,4 @@ Require Export HoTT.Spaces.Int.Core. Require Export HoTT.Spaces.Int.Spec. Require Export HoTT.Spaces.Int.Equiv. -Require Export HoTT.Spaces.Int.LoopExp. \ No newline at end of file +Require Export HoTT.Spaces.Int.LoopExp. diff --git a/theories/Spaces/Pos.v b/theories/Spaces/Pos.v index 686a440e86e..e49ec8c53e3 100644 --- a/theories/Spaces/Pos.v +++ b/theories/Spaces/Pos.v @@ -1,2 +1,2 @@ Require Export HoTT.Spaces.Pos.Core. -Require Export HoTT.Spaces.Pos.Spec. \ No newline at end of file +Require Export HoTT.Spaces.Pos.Spec.