From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 4 Nov 2002 12:45:25 +0000 (+0000)
Subject: - Comments updated
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=87b143efa63a920f7e36d2590ee23a45f450dfce;p=helm.git

- Comments updated
- Eq renamed to eqT
---

diff --git a/helm/gTopLevel/esempi/fourier.cic b/helm/gTopLevel/esempi/fourier.cic
index 09caea79b..a76b4586a 100644
--- a/helm/gTopLevel/esempi/fourier.cic
+++ b/helm/gTopLevel/esempi/fourier.cic
@@ -9,7 +9,7 @@ alias Rminus    /Coq/Reals/Rdefinitions/Rminus.con
 alias R1        /Coq/Reals/Rdefinitions/R1.con
 alias R0        /Coq/Reals/Rdefinitions/R0.con
 alias R        /Coq/Reals/Rdefinitions/R.con
-alias Eq	/Coq/Init/Logic_Type/eqT.ind#1/1
+alias eqT	/Coq/Init/Logic_Type/eqT.ind#1/1
 
 //test base1 ok
 !x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1))
@@ -17,7 +17,7 @@ alias Eq	/Coq/Init/Logic_Type/eqT.ind#1/1
 //test base2 ok
 !x:R.!y:R.(Rlt x y) -> (Rgt (Rplus y R1) (Rminus x R1))
 
-//test base3 (unification fails)
+//test base3 ok
 !x:R.!y:R.(Rge x y) -> (Rlt (Rplus y R1) (Rplus x (Rplus R1 R1)))
 
 //test base4 ok
@@ -26,8 +26,8 @@ alias Eq	/Coq/Init/Logic_Type/eqT.ind#1/1
 //test base5 ok
 !x:R.!y:R.(Rlt x ( Rplus y R1 ) ) -> (Rge (Rplus y (Rplus R1 R1)) (Rminus x R0))
 
-//test base6 (unification fails)
-!x:R.!y:R.(Eq R x y) -> (Rgt (Rplus y R1) (Rminus x R1))
+//test base6 (fourier fails)
+!x:R.!y:R.(eqT R x y) -> (Rgt (Rplus y R1) (Rminus x R1))
 
 //test base7 (should fail) ok
 !x:R.!y:R.(Rlt x y) -> (Rlt (Rplus y R1) (Rminus x R1))