From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 theories/Sets/Finite_sets_facts.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'theories/Sets/Finite_sets_facts.v')

diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v
index 91717f9e..fdcc4150 100644
--- a/theories/Sets/Finite_sets_facts.v
+++ b/theories/Sets/Finite_sets_facts.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Finite_sets_facts.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
 
 Require Export Finite_sets.
 Require Export Constructive_sets.
@@ -72,7 +72,7 @@ Section Finite_sets_facts.
   Proof.
     intros X Y H; induction H as [|A Fin_A Hind x].
     rewrite (Empty_set_zero U Y). trivial.
-    intros. 
+    intros.
     rewrite (Union_commutative U (Add U A x) Y).
     rewrite <- (Union_add U Y A x).
     rewrite (Union_commutative U Y A).
@@ -98,7 +98,7 @@ Section Finite_sets_facts.
   Proof.
     intros A H' X; apply Finite_downward_closed with A; auto with sets.
   Qed.
-  
+
   Lemma cardinalO_empty :
     forall X:Ensemble U, cardinal U X 0 -> X = Empty_set U.
   Proof.
@@ -212,7 +212,7 @@ Section Finite_sets_facts.
   Proof.
     intros; apply cardinal_is_functional with X X; auto with sets.
   Qed.
-  
+
   Lemma card_Add_gen :
     forall (A:Ensemble U) (x:U) (n n':nat),
       cardinal U A n -> cardinal U (Add U A x) n' -> n' <= S n.
@@ -279,7 +279,7 @@ Section Finite_sets_facts.
     intro E; rewrite E; auto with sets arith.
     apply cardinal_unicity with X; auto with sets arith.
   Qed.
-  
+
   Lemma G_aux :
     forall P:Ensemble U -> Prop,
       (forall X:Ensemble U,
-- 
cgit v1.2.3