X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fesempi%2Ffourier.cic;h=a76b4586a2076712830eccd035a83c702f29e0ca;hb=1dd5176f6d6a6247ebf941a1f6319a909f43d5fc;hp=09caea79be6c9617500e850bb255e7c9b15ca5ee;hpb=4e4c541d10848af70ef5cb2ff53e58c02cf8833f;p=helm.git

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))