From: Claudio Sacerdoti Coen Date: Tue, 26 May 2009 11:52:47 +0000 (+0000) Subject: ... X-Git-Tag: make_still_working~3945 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bbbce43b0a27ea3d9b261803f6ce48641ab7998b;p=helm.git ... --- diff --git a/helm/software/matita/tests/ng_tactics.ma b/helm/software/matita/tests/ng_tactics.ma index cf1bbe14a..882bdcbeb 100644 --- a/helm/software/matita/tests/ng_tactics.ma +++ b/helm/software/matita/tests/ng_tactics.ma @@ -31,7 +31,7 @@ nwhd in H: (?%? (?%?)); nchange in match (S ?) in H:(??%?) ⊢ (??%%) with (pred (S ?)); ngeneralize in match H; napply (? H); -nelim m in ⊢ (???(?%?) → %); (*SBAGLIA UNIFICATORE*) +nelim m in ⊢ (???(?%?) → %); nnormalize; ##[ ncases x in H ⊢ (? → % → ?); ##|