- big interface changes: open goals are now collected in a notebook

[helm.git] / helm / gTopLevel / esempi / fourier.cic

diff --git a/helm/gTopLevel/esempi/fourier.cic b/helm/gTopLevel/esempi/fourier.cic
index 09caea79be6c9617500e850bb255e7c9b15ca5ee..a76b4586a2076712830eccd035a83c702f29e0ca 100644 (file)
--- 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))