From: Ferruccio Guidi Date: Thu, 7 Jul 2005 12:20:55 +0000 (+0000) Subject: another bug of auto X-Git-Tag: V_0_7_1~22 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9288eedb2f59a55c78092f78649413fb087310da;p=helm.git another bug of auto --- diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma index 274cda027..7163c56b3 100644 --- a/helm/matita/tests/fguidi.ma +++ b/helm/matita/tests/fguidi.ma @@ -93,6 +93,6 @@ qed. (* theorem le_trans: \forall x,y. (le x y) \to \forall z. (le y z) \to (le x z). intros 1. elim x. -clear H. auto. +clear x. auto. clear H. fwd H1 [H]. decompose H. *) \ No newline at end of file