From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 31 Dec 2006 14:49:11 +0000 (+0000)
Subject: some tests patched
X-Git-Tag: 0.4.95@7852~693
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b70dd6eca72985b11d7d223b8a6a84fda44cdf69;p=helm.git

some tests patched
---

diff --git a/matita/tests/dependent_injection.ma b/matita/tests/dependent_injection.ma
index 069c75297..2f4bbe820 100644
--- a/matita/tests/dependent_injection.ma
+++ b/matita/tests/dependent_injection.ma
@@ -33,8 +33,8 @@ inductive ttree : Type → Type :=
     (that state the existence of a ?1 such that ...) *)
 theorem injection_test3:
  ∀t,t'. tnode nat t tempty = tnode nat t' tempty → t = t'.
- intros;
- destruct H;
+ intros.
+ destruct H.
  assumption.
 qed.
 
diff --git a/matita/tests/fguidi.ma b/matita/tests/fguidi.ma
index 84faee59a..b1c17185d 100644
--- a/matita/tests/fguidi.ma
+++ b/matita/tests/fguidi.ma
@@ -42,7 +42,7 @@ definition pred: nat \to nat \def
       ]. 
 
 theorem eq_gen_S_O: \forall x. (S x = O) \to \forall P:Prop. P.
-intros. apply False_ind. cut (is_S O). auto new. elim H. exact I.
+intros. apply False_ind. cut (is_S O). elim Hcut. rewrite < H. apply I.
 qed.
 
 theorem eq_gen_S_O_cc: (\forall P:Prop. P) \to \forall x. (S x = O).
@@ -81,9 +81,11 @@ qed.
 
 theorem le_gen_S_x_aux: \forall m,x,y. (le y x) \to (y = S m) \to 
                         (\exists n. x = (S n) \land (le m n)).
-intros 4. elim H. 
+intros 4. elim H; clear H x y.
 apply eq_gen_S_O. exact m. elim H1. auto paramodulation.
-cut (n = m). elim Hcut. apply ex_intro. exact n1. auto new.auto paramodulation.
+clear H2. cut (n = m).
+elim Hcut. apply ex_intro. exact n1. split; auto.
+apply eq_gen_S_S. auto.
 qed.
 
 theorem le_gen_S_x: \forall m,x. (le (S m) x) \to 
diff --git a/matita/tests/record.ma b/matita/tests/record.ma
index c024acf9e..1c73c8951 100644
--- a/matita/tests/record.ma
+++ b/matita/tests/record.ma
@@ -41,4 +41,4 @@ record paperino: Prop \def {
 (* the following test used to show the following bug: the left
    parameter A in the type of t was not unified with the left
    parameter A in the type of the constructor of the record *)
-record t A : Type := { f : t A }.
+record t (A:Type) : Type := { f : t A }.