fix

diff --git a/helm/matita/tests/apply.ma b/helm/matita/tests/apply.ma
index e53d315f0339c8dd2053bf3203685cbd7ff06c25..0fcf73cf32fc81cbf60dc44c4549116e69df5ec9 100644 (file)
--- a/helm/matita/tests/apply.ma
+++ b/helm/matita/tests/apply.ma
@@ -18,8 +18,8 @@ alias symbol "eq" (instance 0) = "leibnitz's equality".
 
 theorem a:
   \forall A:Set.
-  \forall x,y : A.
-  not (x=y) \to not (x=y).
+  \forall x: A.
+  not (x=x) \to not (x=x).
 intros.
 apply H.
 qed.

diff --git a/helm/matita/tests/clearbody.ma b/helm/matita/tests/clearbody.ma
index b38de22dbd0ec3866a7d20f2127dce94f677b3cb..29dd2457dae94317c6561786c206d2bb07743e51 100644 (file)
--- a/helm/matita/tests/clearbody.ma
+++ b/helm/matita/tests/clearbody.ma
@@ -19,7 +19,7 @@ alias symbol "plus" (instance 0) = "natural plus".
 
 
 theorem stupid : 
-  let x \def 0 + 1 in x + 1= x + 1.
+  let x \def 0 + 1 in x + 2 = x + 2.
   intros.
   clearbody x. 
   simplify.

diff --git a/helm/matita/tests/constructor.ma b/helm/matita/tests/constructor.ma
index 3b9c21c81a22bee137bba387b51eee441997937c..5f9bed6c01dcb9cd39a0a82e12502d02a80f234e 100644 (file)
--- a/helm/matita/tests/constructor.ma
+++ b/helm/matita/tests/constructor.ma
@@ -17,6 +17,6 @@ alias num (instance 0) = "natural number".
 alias symbol "eq" (instance 0) = "leibnitz's equality".
 
 
-theorem stupid: 0 = 0.
+theorem stupid: 1 = 1.
 constructor 1.
 qed.

diff --git a/helm/matita/tests/contradiction.ma b/helm/matita/tests/contradiction.ma
index ddd9ac878b4246ce6335f565a978d2004897e98f..d5199aefc1ce02c563a3eb2fc748bde0138f8add 100644 (file)
--- a/helm/matita/tests/contradiction.ma
+++ b/helm/matita/tests/contradiction.ma
@@ -20,7 +20,7 @@ alias symbol "eq" (instance 0) = "leibnitz's equality".
 
 
 
-theorem stupid: \forall a:Prop. a \to not a \to 0 = 1.
+theorem stupid: \forall a:Prop. a \to not a \to 0 = 2.
 intros.
 letin H \def (H1 H).
 contradiction.

diff --git a/helm/matita/tests/cut.ma b/helm/matita/tests/cut.ma
index 8ba63bd8b9959898f28d98a4fbbf2f17c96915db..82d36667b6d6daffa900f638eb3d856530a02cb5 100644 (file)
--- a/helm/matita/tests/cut.ma
+++ b/helm/matita/tests/cut.ma
@@ -16,8 +16,8 @@ set "baseuri" "cic:/matita/tests/cut".
 alias num (instance 0) = "natural number".
 alias symbol "eq" (instance 0) = "leibnitz's equality".
 
-theorem stupid: 0 = 0.
-  cut 0 = 0.
+theorem stupid: 3 = 3.
+  cut 3 = 3.
   assumption.
   reflexivity.
   qed.