X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FPREDICATIVE-TOPOLOGY%2Fclass_eq.ma;h=b86e5f2961f79d60ef75010320b10aab72820feb;hb=dd4b01b7fbd69a4af86ec5d41eb5da39a27e4a64;hp=6773470b0bf1cce469498fb0dacb4a6a15bcefda;hpb=15a4250eae08063fc14e2448dcb90e55b4850384;p=helm.git

diff --git a/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma b/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma
index 6773470b0..b86e5f296 100644
--- a/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma
+++ b/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma
@@ -23,10 +23,10 @@ theorem ceq_trans: \forall C. \xforall c1,c2. ceq C c1 c2 \to
 intros.
 
 (*
-apply ceq_intro; apply cle_trans; [|auto|auto||auto|auto].
+apply ceq_intro; apply cle_trans; [|auto new timeout=100|auto new timeout=100||auto new timeout=100|auto new timeout=100].
 qed.
 
 theorem ceq_sym: \forall C,c1,c2. ceq C c1 c2 \to ceq C c2 c1.
-intros; elim H; clear H.; auto.
+intros; elim H; clear H.; auto new timeout=100.
 qed.
 *)