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

---
 test-suite/modules/Przyklad.v | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'test-suite/modules/Przyklad.v')

diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v
index 014f6c60..e3694b81 100644
--- a/test-suite/modules/Przyklad.v
+++ b/test-suite/modules/Przyklad.v
@@ -1,4 +1,4 @@
-Definition ifte (T : Set) (A B : Prop) (s : {A} + {B}) 
+Definition ifte (T : Set) (A B : Prop) (s : {A} + {B})
   (th el : T) := if s then th else el.
 
 Implicit Arguments ifte.
@@ -33,7 +33,7 @@ Module Type ELEM.
   Parameter T : Set.
   Parameter eq_dec : forall a a' : T, {a = a'} + {a <> a'}.
 End ELEM.
-                                        
+
 Module Type SET (Elt: ELEM).
   Parameter T : Set.
   Parameter empty : T.
@@ -104,11 +104,11 @@ Module Nat.
 End Nat.
 
 
-Module SetNat := F Nat. 
+Module SetNat := F Nat.
 
 
-Lemma no_zero_in_empty : SetNat.find 0 SetNat.empty = false. 
-apply SetNat.find_empty_false. 
+Lemma no_zero_in_empty : SetNat.find 0 SetNat.empty = false.
+apply SetNat.find_empty_false.
 Qed.
 
 (***************************************************************************)
@@ -120,8 +120,8 @@ Module Lemmas (G: SET) (E: ELEM).
    forall (S : ESet.T) (a1 a2 : E.T),
    let S1 := ESet.add a1 (ESet.add a2 S) in
    let S2 := ESet.add a2 (ESet.add a1 S) in
-   forall a : E.T, ESet.find a S1 = ESet.find a S2. 
-  
+   forall a : E.T, ESet.find a S1 = ESet.find a S2.
+
     intros.
     unfold S1, S2 in |- *.
     elim (E.eq_dec a a1); elim (E.eq_dec a a2); intros H1 H2;
@@ -137,10 +137,10 @@ Inductive list (A : Set) : Set :=
   | nil : list A
   | cons : A -> list A -> list A.
 
-Module ListDict (E: ELEM). 
+Module ListDict (E: ELEM).
   Definition T := list E.T.
   Definition elt := E.T.
-   
+
   Definition empty := nil elt.
   Definition add (e : elt) (s : T) := cons elt e s.
   Fixpoint find (e : elt) (s : T) {struct s} : bool :=
@@ -160,7 +160,7 @@ Module ListDict (E: ELEM).
     auto.
 
   Qed.
-  
+
 
   Lemma find_add_false :
    forall (s : T) (e e' : E.T), e <> e' -> find e (add e' s) = find e s.
@@ -171,8 +171,8 @@ Module ListDict (E: ELEM).
      rewrite H0.
     simpl in |- *.
     reflexivity.
-  Qed.    
-  
+  Qed.
+
 
 End ListDict.
 
-- 
cgit v1.2.3