some tests patched

diff --git a/matita/tests/dependent_injection.ma b/matita/tests/dependent_injection.ma
index 069c7529744115802f655e2cd69b3f7a3ddb113a..2f4bbe82057fd4d15f498cdf0d978d54dce1a470 100644 (file)
--- 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 84faee59ace814a772bacd076c95c6c6ef7ec662..b1c17185d08dfabb33aff29c2576307ad7cb59fb 100644 (file)
--- 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 c024acf9e029c6a81a2f848a0902bca967390a01..1c73c8951411c4e9eb1a47b2a8dd5a1c5bcaa588 100644 (file)
--- 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 }.