coinduction is between us

[helm.git] / helm / software / matita / tests / ng_tactics.ma

diff --git a/helm/software/matita/tests/ng_tactics.ma b/helm/software/matita/tests/ng_tactics.ma
index cf1bbe14abd2474460d50a06ae368ab82b02e23e..882bdcbeb1e89856ea2954c81875382ef463a2de 100644 (file)
--- 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 ⊢ (? → % → ?);
  ##|