From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 29 Sep 2006 14:49:31 +0000 (+0000)
Subject: fixed (dasabled paramod)
X-Git-Tag: make_still_working~6828
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=inline;h=ffce9e00cc481f80416f011c52475e70e043a0fa;p=helm.git

fixed (dasabled paramod)
---

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.