- init_cache_and_tables rewritten using the automation_cache

[helm.git] / helm / software / matita / library / nat / gcd.ma

diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma
index b970fb0c3ba1b1f1096cead8eb4951f1f2dafa87..958fddf970207216bfcab426a8389e202a942786 100644 (file)
--- a/helm/software/matita/library/nat/gcd.ma
+++ b/helm/software/matita/library/nat/gcd.ma
@@ -761,7 +761,8 @@ cut (n \divides p \lor n \ndivides p)
           rewrite > (sym_times q (a1*p)).
           rewrite > (assoc_times a1).
           elim H1.
-          applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
+          pump 39.
+          applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).          
           (*
           rewrite < (sym_times n).rewrite < assoc_times.
           rewrite > (sym_times q).rewrite > assoc_times.