From c34722e7f8ca26ed55a63a02dbfd7f3c4d2038b5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 9 Oct 2006 18:18:24 +0000 Subject: [PATCH] added to applyS in nat/gcd.ma a timeout large enough for compilation in bytecode mode. --- matita/library/nat/gcd.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/matita/library/nat/gcd.ma b/matita/library/nat/gcd.ma index 6ce4f538e..fdb1e8d90 100644 --- a/matita/library/nat/gcd.ma +++ b/matita/library/nat/gcd.ma @@ -520,7 +520,7 @@ cut (n \divides p \lor n \ndivides p) elim H1.rewrite > H6. (* applyS (witness n (n*(q*a-a1*n2)) (q*a-a1*n2)) reflexivity. *); - applyS (witness n ? ? (refl_eq ? ?)). + applyS (witness n ? ? (refl_eq ? ?)) timeout=50. (* rewrite < (sym_times n).rewrite < assoc_times. rewrite > (sym_times q).rewrite > assoc_times. -- 2.39.2