From e9278f62d563a431eaaa472967bec00293f378f0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 20 Mar 2008 12:42:45 +0000 Subject: [PATCH] letins are no more unfolded, we do that by hand --- helm/software/matita/tests/bad_induction.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.39.2