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/bugs/closed/shouldsucceed/846.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'test-suite/bugs/closed/shouldsucceed/846.v')

diff --git a/test-suite/bugs/closed/shouldsucceed/846.v b/test-suite/bugs/closed/shouldsucceed/846.v
index a963b225..ee5ec1fa 100644
--- a/test-suite/bugs/closed/shouldsucceed/846.v
+++ b/test-suite/bugs/closed/shouldsucceed/846.v
@@ -27,7 +27,7 @@ Definition index := list bool.
 
 Inductive L (A:Set) : index -> Set :=
   initL: A -> L A nil
-  | pluslL: forall l:index, One -> L A (false::l) 
+  | pluslL: forall l:index, One -> L A (false::l)
   | plusrL: forall l:index, L A l -> L A (false::l)
   | varL: forall l:index, L A l -> L A (true::l)
   | appL: forall l:index, L A (true::l) -> L A (true::l) -> L A (true::l)
@@ -109,7 +109,7 @@ Proof.
   exact (monL (fun x:One + A =>
     (match (maybe (fun a:A => initL a) x) with
        | inl u => pluslL _ _ u
-       | inr t' => plusrL t' end)) r). 
+       | inr t' => plusrL t' end)) r).
 Defined.
 
 Section minimal.
@@ -119,11 +119,11 @@ Hypothesis G: Set -> Set.
 Hypothesis step: sub1 (LamF' G) G.
 
 Fixpoint L'(A:Set)(i:index){struct i} : Set :=
-  match i with 
+  match i with
     nil => A
     | false::l => One + L' A l
     | true::l => G (L' A l)
-  end. 
+  end.
 
 Definition LinL': forall (A:Set)(i:index), L A i -> L' A i.
 Proof.
@@ -177,7 +177,7 @@ Proof.
   assumption.
   induction a.
   simpl L' in t.
-  apply (aczelapp (l1:=true::nil) (l2:=i)). 
+  apply (aczelapp (l1:=true::nil) (l2:=i)).
   exact (lam' IHi t).
   simpl L' in t.
   induction t.
-- 
cgit v1.2.3