diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-21 18:29:07 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-21 18:29:07 +0200 |
commit | 9dea4814ae928192e23764c09473501e2ecc9937 (patch) | |
tree | 8fef19360dd8ca299d31369534a729b4925f7a4c /theories | |
parent | 325890a83a2b073d9654b5615c585cd65a376fbd (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.v | 2 | ||||
-rw-r--r-- | theories/FSets/FSets.v | 2 | ||||
-rw-r--r-- | theories/MSets/MSetGenTree.v | 2 | ||||
-rw-r--r-- | theories/MSets/MSets.v | 2 | ||||
-rw-r--r-- | theories/NArith/BinNatDef.v | 2 | ||||
-rw-r--r-- | theories/Numbers/NatInt/NZParity.v | 2 | ||||
-rw-r--r-- | theories/Program/Tactics.v | 2 | ||||
-rw-r--r-- | theories/QArith/Qcabs.v | 2 | ||||
-rw-r--r-- | theories/Reals/Ranalysis.v | 2 | ||||
-rw-r--r-- | theories/Vectors/Vector.v | 2 | ||||
-rw-r--r-- | theories/ZArith/BinIntDef.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Zsqrt_compat.v | 2 |
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. |