From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 11 Jul 2005 14:10:43 +0000 (+0000)
Subject: fix
X-Git-Tag: pre_notation~42
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9f7cb5462119ce44becf0bc9848d61690a048ac7;p=helm.git

fix
---

diff --git a/helm/matita/tests/apply.ma b/helm/matita/tests/apply.ma
index e53d315f0..0fcf73cf3 100644
--- 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 b38de22db..29dd2457d 100644
--- 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 3b9c21c81..5f9bed6c0 100644
--- 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 ddd9ac878..d5199aefc 100644
--- 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 8ba63bd8b..82d36667b 100644
--- 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.