From 3bca0281034722fbbd3a45b16ae841ef54c317ca Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 1 Mar 2017 15:21:37 -0500
Subject: Remove some trailing whitespace in Init/Specif.v

---
 theories/Init/Specif.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 9fc00e80c1..e94b2e3468 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -103,7 +103,7 @@ Definition sig_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sig P
     of an [a] of type [A], a of a proof [h] that [a] satisfies [P],
     and a proof [h'] that [a] satisfies [Q].  Then
     [(proj1_sig (sig_of_sig2 y))] is the witness [a],
-    [(proj2_sig (sig_of_sig2 y))] is the proof of [(P a)], and 
+    [(proj2_sig (sig_of_sig2 y))] is the proof of [(P a)], and
     [(proj3_sig y)] is the proof of [(Q a)]. *)
 
 Section Subset_projections2.
@@ -263,10 +263,10 @@ Section Dependent_choice_lemmas.
     (forall x:X, {y | R x y}) ->
     forall x0, {f : nat -> X | f O = x0 /\ forall n, R (f n) (f (S n))}.
   Proof.
-    intros H x0. 
+    intros H x0.
     set (f:=fix f n := match n with O => x0 | S n' => proj1_sig (H (f n')) end).
     exists f.
-    split. reflexivity. 
+    split. reflexivity.
     induction n; simpl; apply proj2_sig.
   Defined.
 
-- 
cgit v1.2.3