From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 6 May 2010 15:52:38 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~2909
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3b6ca0e12de74ada4da4a3500a0cbffaa260c9e1;hp=668fb315dc8502dc1b4d336eba19ab9436bf5b7a;p=helm.git

...
---

diff --git a/helm/software/matita/nlibrary/PTS/subst.ma b/helm/software/matita/nlibrary/PTS/subst.ma
index 5282e86ba..77455d4cb 100644
--- a/helm/software/matita/nlibrary/PTS/subst.ma
+++ b/helm/software/matita/nlibrary/PTS/subst.ma
@@ -107,7 +107,7 @@ napply (leb_elim (S n) k); nnormalize; #Hnk;
   ##[nrewrite > (le_to_leb_true ?? Hnk);nnormalize;//;
   ##|nrewrite > (lt_to_leb_false (S (n + 1)) k ?); nnormalize;
       ##[nrewrite > (not_eq_to_eqb_false (n+1) k ?);
-         nnormalize;/2/; napply (not_to_not … Hnk);//;
+         nnormalize;/2/
       ##|napply le_S; napplyS (not_le_to_lt (S n) k Hnk);
       ##]
   ##]