X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Ftests%2Fng_tactics.ma;h=629c9990920b6d32c370c731d30a54323fe874f3;hb=75514fe2207992ebc549822a7cbd5d37688690ac;hp=dff3db699b2303f50c2cc1b0e42129416be05e3b;hpb=1ceab612eaa241f09a60073fc8a58acac6f35a37;p=helm.git

diff --git a/helm/software/matita/tests/ng_tactics.ma b/helm/software/matita/tests/ng_tactics.ma
index dff3db699..629c99909 100644
--- a/helm/software/matita/tests/ng_tactics.ma
+++ b/helm/software/matita/tests/ng_tactics.ma
@@ -21,7 +21,7 @@ nletin pippo ≝ (S m) in H: % ⊢ (???%);
             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);
-nwhd in H:(???%);
+ngeneralize in match m in ⊢ %; (* BUG *)
 STOP;
 
 nwhd in H:(???%);