From 1fb4a3751e889ec66bd5263a9813415053e63cd3 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. --- helm/software/matita/library/nat/gcd.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma index 6ce4f538e..fdb1e8d90 100644 --- a/helm/software/matita/library/nat/gcd.ma +++ b/helm/software/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.5