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/success/coercions.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'test-suite/success/coercions.v')

diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v
index 525348de..908b5f77 100644
--- a/test-suite/success/coercions.v
+++ b/test-suite/success/coercions.v
@@ -24,7 +24,7 @@ Coercion C : nat >-> Funclass.
 
 (* Remark: in the following example, it cannot be decided whether C is
    from nat to Funclass or from A to nat. An explicit Coercion command is
-   expected 
+   expected
 
 Parameter A : nat -> Prop.
 Parameter C:> forall n:nat, A n -> nat.
@@ -71,7 +71,6 @@ Record Morphism (X Y:Setoid) : Type :=
 {evalMorphism :> X -> Y}.
 
 Definition extSetoid (X Y:Setoid) : Setoid.
-intros X Y.
 constructor.
 exact (Morphism X Y).
 Defined.
-- 
cgit v1.2.3