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/typeclasses/clrewrite.v | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'test-suite/typeclasses/clrewrite.v')

diff --git a/test-suite/typeclasses/clrewrite.v b/test-suite/typeclasses/clrewrite.v
index 2978fda2..f21acd4c 100644
--- a/test-suite/typeclasses/clrewrite.v
+++ b/test-suite/typeclasses/clrewrite.v
@@ -15,7 +15,7 @@ Section Equiv.
   Qed.
 
   Tactic Notation "simpl" "*" := auto || relation_tac.
-  
+
   Goal eqA x y -> eqA y x /\ True.
     intros H ; clrewrite H.
     split ; simpl*.
@@ -27,13 +27,13 @@ Section Equiv.
   Qed.
 
   Goal eqA x y -> eqA y z -> eqA x y.
-    intros H. 
+    intros H.
     clrewrite H.
     intro. refl.
   Qed.
-        
+
   Goal eqA x y -> eqA z y -> eqA x y.
-    intros H. 
+    intros H.
     clrewrite <- H at 2.
     clrewrite <- H at 1.
     intro. refl.
@@ -54,7 +54,7 @@ Section Equiv.
     clrewrite <- H.
     refl.
   Qed.
-  
+
   Goal eqA x y -> True /\ True /\ False /\ eqA x x -> True /\ True /\ False /\ eqA x y.
   Proof.
     intros.
@@ -70,12 +70,12 @@ Section Trans.
   Variables x y z w : A.
 
   Tactic Notation "simpl" "*" := auto || relation_tac.
-  
+
 (*   Typeclasses eauto := debug. *)
 
   Goal R x y -> R y x -> R y y -> R x x.
   Proof with auto.
-    intros H H' H''. 
+    intros H H' H''.
 
     clrewrite <- H' at 2.
     clrewrite H at 1...
@@ -86,11 +86,11 @@ Section Trans.
     clrewrite H.
     refl.
   Qed.
-        
+
   Goal R x y -> R z y -> R x y.
-    intros H. 
+    intros H.
     clrewrite <- H at 2.
-    intro. 
+    intro.
     clrewrite H at 1.
   Abort.
 
-- 
cgit v1.2.3