From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 20 Mar 2008 12:42:45 +0000 (+0000)
Subject: letins are no more unfolded, we do that by hand
X-Git-Tag: make_still_working~5517
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e9278f62d563a431eaaa472967bec00293f378f0;p=helm.git

letins are no more unfolded, we do that by hand
---

diff --git a/helm/software/matita/tests/bad_induction.ma b/helm/software/matita/tests/bad_induction.ma
index 172aa8e11..99c6b5898 100644
--- a/helm/software/matita/tests/bad_induction.ma
+++ b/helm/software/matita/tests/bad_induction.ma
@@ -23,5 +23,5 @@ axiom bad_ind : ∀P : nat -> Prop. ∀n.(n = O -> P n) -> (∀n.P n -> P (S n))
 theorem absurd: ∀n. n = O.
   intros.
   letin P ≝ (λx:nat. n = O).
-  apply (bad_ind P n); simplify; intros; autobatch.
+  apply (bad_ind P n); simplify; intros; unfold; autobatch.
 qed.
\ No newline at end of file