aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-08-21 18:29:07 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-08-21 18:29:07 +0200
commit9dea4814ae928192e23764c09473501e2ecc9937 (patch)
tree8fef19360dd8ca299d31369534a729b4925f7a4c /theories
parent325890a83a2b073d9654b5615c585cd65a376fbd (diff)
Ensuring all .v files end with a newline to make "sed -i" work better on them.
Diffstat (limited to 'theories')
-rw-r--r--theories/Arith/Peano_dec.v2
-rw-r--r--theories/FSets/FSets.v2
-rw-r--r--theories/MSets/MSetGenTree.v2
-rw-r--r--theories/MSets/MSets.v2
-rw-r--r--theories/NArith/BinNatDef.v2
-rw-r--r--theories/Numbers/NatInt/NZParity.v2
-rw-r--r--theories/Program/Tactics.v2
-rw-r--r--theories/QArith/Qcabs.v2
-rw-r--r--theories/Reals/Ranalysis.v2
-rw-r--r--theories/Vectors/Vector.v2
-rw-r--r--theories/ZArith/BinIntDef.v2
-rw-r--r--theories/ZArith/Zsqrt_compat.v2
12 files changed, 12 insertions, 12 deletions
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.