From 51c08664500a2da69644dc168da5d07f279ca992 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 29 Sep 2006 14:49:31 +0000 Subject: [PATCH] fixed (dasabled paramod) --- matita/tests/bad_tests/auto.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/matita/tests/bad_tests/auto.ma b/matita/tests/bad_tests/auto.ma index c7bd62492..12fa478bb 100755 --- a/matita/tests/bad_tests/auto.ma +++ b/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