From 9dea4814ae928192e23764c09473501e2ecc9937 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Mon, 21 Aug 2017 18:29:07 +0200
Subject: Ensuring all .v files end with a newline to make "sed -i" work better
 on them.

---
 theories/Arith/Peano_dec.v         | 2 +-
 theories/FSets/FSets.v             | 2 +-
 theories/MSets/MSetGenTree.v       | 2 +-
 theories/MSets/MSets.v             | 2 +-
 theories/NArith/BinNatDef.v        | 2 +-
 theories/Numbers/NatInt/NZParity.v | 2 +-
 theories/Program/Tactics.v         | 2 +-
 theories/QArith/Qcabs.v            | 2 +-
 theories/Reals/Ranalysis.v         | 2 +-
 theories/Vectors/Vector.v          | 2 +-
 theories/ZArith/BinIntDef.v        | 2 +-
 theories/ZArith/Zsqrt_compat.v     | 2 +-
 12 files changed, 12 insertions(+), 12 deletions(-)

(limited to 'theories')

diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 88cda79d8..247ea20a8 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -57,4 +57,4 @@ now rewrite H.
 Qed.
 
 (** For compatibility *)
-Require Import Le Lt.
\ No newline at end of file
+Require Import Le Lt.
diff --git a/theories/FSets/FSets.v b/theories/FSets/FSets.v
index 572f28654..e03fb2236 100644
--- a/theories/FSets/FSets.v
+++ b/theories/FSets/FSets.v
@@ -20,4 +20,4 @@ Require Export FSetEqProperties.
 Require Export FSetWeakList.
 Require Export FSetList.
 Require Export FSetPositive.
-Require Export FSetAVL.
\ No newline at end of file
+Require Export FSetAVL.
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
index 036ff1aa4..9fb8e499b 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -1144,4 +1144,4 @@ Proof.
  apply mindepth_cardinal.
 Qed.
 
-End Props.
\ No newline at end of file
+End Props.
diff --git a/theories/MSets/MSets.v b/theories/MSets/MSets.v
index f179bcd1d..1ee485cc1 100644
--- a/theories/MSets/MSets.v
+++ b/theories/MSets/MSets.v
@@ -18,4 +18,4 @@ Require Export MSetEqProperties.
 Require Export MSetWeakList.
 Require Export MSetList.
 Require Export MSetPositive.
-Require Export MSetAVL.
\ No newline at end of file
+Require Export MSetAVL.
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index ba923d062..6771e57ad 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -378,4 +378,4 @@ Definition iter (n:N) {A} (f:A->A) (x:A) : A :=
     | pos p => Pos.iter f x p
   end.
 
-End N.
\ No newline at end of file
+End N.
diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v
index de3bbbca7..626d59d73 100644
--- a/theories/Numbers/NatInt/NZParity.v
+++ b/theories/Numbers/NatInt/NZParity.v
@@ -260,4 +260,4 @@ Proof.
  intros. apply odd_add_mul_even. apply even_spec, even_2.
 Qed.
 
-End NZParityProp.
\ No newline at end of file
+End NZParityProp.
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 9aca56f47..b06562fc4 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -328,4 +328,4 @@ Ltac program_simpl := program_simplify ; try typeclasses eauto with program ; tr
 
 Obligation Tactic := program_simpl.
 
-Definition obligation (A : Type) {a : A} := a.
\ No newline at end of file
+Definition obligation (A : Type) {a : A} := a.
diff --git a/theories/QArith/Qcabs.v b/theories/QArith/Qcabs.v
index 1883c77be..09908665e 100644
--- a/theories/QArith/Qcabs.v
+++ b/theories/QArith/Qcabs.v
@@ -126,4 +126,4 @@ Proof.
   destruct (proj1 (Qcabs_Qcle_condition x 0)) as [A B].
   + rewrite H; apply Qcle_refl.
   + apply Qcle_antisym; auto.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v
index 66e37e867..9b0357f03 100644
--- a/theories/Reals/Ranalysis.v
+++ b/theories/Reals/Ranalysis.v
@@ -26,4 +26,4 @@ Require Export RList.
 Require Export Sqrt_reg.
 Require Export Ranalysis4.
 Require Export Rpower.
-Require Export Ranalysis_reg.
\ No newline at end of file
+Require Export Ranalysis_reg.
diff --git a/theories/Vectors/Vector.v b/theories/Vectors/Vector.v
index 672858fa5..19d749fc8 100644
--- a/theories/Vectors/Vector.v
+++ b/theories/Vectors/Vector.v
@@ -21,4 +21,4 @@ Require VectorSpec.
 Require VectorEq.
 Include VectorDef.
 Include VectorSpec.
-Include VectorEq.
\ No newline at end of file
+Include VectorEq.
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index 7686fbae8..443667f48 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -616,4 +616,4 @@ Definition lxor a b :=
    | neg a, neg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b))
  end.
 
-End Z.
\ No newline at end of file
+End Z.
diff --git a/theories/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v
index fb7f71b4b..cccd970da 100644
--- a/theories/ZArith/Zsqrt_compat.v
+++ b/theories/ZArith/Zsqrt_compat.v
@@ -229,4 +229,4 @@ Proof.
  symmetry. apply Z.sqrt_unique; trivial.
  now apply Zsqrt_interval.
  now destruct n.
-Qed.
\ No newline at end of file
+Qed.
-- 
cgit v1.2.3