From eff920e57112c3eaee889384d435602e41951a36 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 16 Apr 2009 15:31:10 +0000 Subject: [PATCH] Bug: let-ins are always automatically folded! --- helm/software/matita/tests/ng_tactics.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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:(???%); -- 2.39.2