X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Ftests%2Fng_tactics.ma;h=629c9990920b6d32c370c731d30a54323fe874f3;hb=d3548c16f481b14ce94e64c790bc767c59590050;hp=a9cb8557787d1c5669ce54a66a988419af8e18e9;hpb=901ee87aad4ae08a19399f8bf925dfdffd92aee1;p=helm.git

diff --git a/helm/software/matita/tests/ng_tactics.ma b/helm/software/matita/tests/ng_tactics.ma
index a9cb85577..629c99909 100644
--- a/helm/software/matita/tests/ng_tactics.ma
+++ b/helm/software/matita/tests/ng_tactics.ma
@@ -18,7 +18,10 @@ ntheorem test1 : ∀n:nat.n = S n + n → S n = (S (S n)).
 #m; #H;
                                  nassert m:nat H: (m=S m + m) ⊢ (S m = S (S m));
 nletin pippo ≝ (S m) in H: % ⊢ (???%);
- nassert m:nat pippo : nat ≝ (S m) ⊢ (m = pippo + m → (S m) = (S pippo));
+            nassert m:nat pippo : nat ≝ (S m) ⊢ (m = pippo + m → S m = S pippo);
+#H; nchange in match pippo in H:% with (pred (S pippo));
+ nassert m:nat pippo : nat ≝ (S m) H:(m = pred (S pippo) + m) ⊢ (S m = S pippo);
+ngeneralize in match m in ⊢ %; (* BUG *)
 STOP;
 
 nwhd in H:(???%);