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/1507.v | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

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

diff --git a/test-suite/bugs/closed/shouldsucceed/1507.v b/test-suite/bugs/closed/shouldsucceed/1507.v
index b484c7dc..f1872a2b 100644
--- a/test-suite/bugs/closed/shouldsucceed/1507.v
+++ b/test-suite/bugs/closed/shouldsucceed/1507.v
@@ -2,16 +2,16 @@
    Implementing reals a la Stolzenberg
 
    Danko Ilik, March 2007
-   svn revision: $Id: 1507.v 10068 2007-08-10 12:06:59Z notin $
+   svn revision: $Id$
 
    XField.v -- (unfinished) axiomatisation of the theories of real and
                rational intervals.
 *)
 
-Definition associative (A:Type)(op:A->A->A) := 
+Definition associative (A:Type)(op:A->A->A) :=
   forall x y z:A, op (op x y) z = op x (op y z).
 
-Definition commutative (A:Type)(op:A->A->A) := 
+Definition commutative (A:Type)(op:A->A->A) :=
   forall x y:A, op x y = op y x.
 
 Definition trichotomous (A:Type)(R:A->A->Prop) :=
@@ -19,7 +19,7 @@ Definition trichotomous (A:Type)(R:A->A->Prop) :=
 
 Definition relation (A:Type) := A -> A -> Prop.
 Definition reflexive (A:Type)(R:relation A) := forall x:A, R x x.
-Definition transitive (A:Type)(R:relation A) := 
+Definition transitive (A:Type)(R:relation A) :=
   forall x y z:A, R x y -> R y z -> R x z.
 Definition symmetric (A:Type)(R:relation A) := forall x y:A, R x y -> R y x.
 
@@ -52,7 +52,7 @@ Record I (grnd:Set)(le:grnd->grnd->Prop) : Type := Imake {
   Iplus_opp_r    : forall x:Icar, Ic (Iplus x (Iopp x)) (Izero);
   Imult_inv_r    : forall x:Icar, ~(Ic x Izero) -> Ic (Imult x (Iinv x)) Ione;
   (* distributive laws *)
-  Imult_plus_distr_l : forall x x' y y' z z' z'', 
+  Imult_plus_distr_l : forall x x' y y' z z' z'',
     Ic x x' -> Ic y y' -> Ic z z' -> Ic z z'' ->
     Ic (Imult (Iplus x y) z) (Iplus (Imult x' z') (Imult y' z''));
   (* order and lattice structure *)
@@ -70,7 +70,7 @@ Record I (grnd:Set)(le:grnd->grnd->Prop) : Type := Imake {
   Ic_sym    : symmetric _ Ic
 }.
 
-Definition interval_set (X:Set)(le:X->X->Prop) := 
+Definition interval_set (X:Set)(le:X->X->Prop) :=
   (interval X le) -> Prop. (* can be Set as well *)
 Check interval_set.
 Check Ic.
@@ -101,7 +101,7 @@ Record N (grnd:Set)(le:grnd->grnd->Prop)(grndI:I grnd le) : Type := Nmake {
   Nplus_opp_r    : forall x:Ncar, Nc (Nplus x (Nopp x)) (Nzero);
   Nmult_inv_r    : forall x:Ncar, ~(Nc x Nzero) -> Nc (Nmult x (Ninv x)) None;
   (* distributive laws *)
-  Nmult_plus_distr_l : forall x x' y y' z z' z'', 
+  Nmult_plus_distr_l : forall x x' y y' z z' z'',
     Nc x x' -> Nc y y' -> Nc z z' -> Nc z z'' ->
     Nc (Nmult (Nplus x y) z) (Nplus (Nmult x' z') (Nmult y' z''));
   (* order and lattice structure *)
-- 
cgit v1.2.3