From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 16 Apr 2009 15:28:37 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~4073
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1ceab612eaa241f09a60073fc8a58acac6f35a37;p=helm.git

...
---

diff --git a/helm/software/matita/tests/ng_tactics.ma b/helm/software/matita/tests/ng_tactics.ma
index a9cb85577..dff3db699 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);
+nwhd in H:(???%);
 STOP;
 
 nwhd in H:(???%);