From 9288eedb2f59a55c78092f78649413fb087310da Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 7 Jul 2005 12:20:55 +0000 Subject: [PATCH] another bug of auto --- helm/matita/tests/fguidi.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.39.2