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

fixed (dasabled paramod)
---

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.