From ffce9e00cc481f80416f011c52475e70e043a0fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 29 Sep 2006 14:49:31 +0000 Subject: [PATCH] fixed (dasabled paramod) --- helm/software/matita/tests/bad_tests/auto.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/tests/bad_tests/auto.ma b/helm/software/matita/tests/bad_tests/auto.ma index c7bd62492..12fa478bb 100755 --- a/helm/software/matita/tests/bad_tests/auto.ma +++ b/helm/software/matita/tests/bad_tests/auto.ma @@ -24,4 +24,4 @@ alias symbol "plus" (instance 0) = "Coq's natural plus". alias symbol "times" (instance 0) = "Coq's natural times". theorem a : \forall x,y:nat. x*x+(S y) = O - x. intros. -auto depth = 3. +auto depth = 4 width = 3 use_paramod = false. -- 2.39.2