From 4a6efdc6425f738fa28622c5f2271c2b5bc96415 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Tue, 4 Jun 2024 20:59:23 +0200 Subject: [PATCH] Greatly reduce the compilation time of src/Arithmetic/BarrettReduction.v. --- src/Arithmetic/BarrettReduction.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Arithmetic/BarrettReduction.v b/src/Arithmetic/BarrettReduction.v index 89173e4e1c..fb35d6cefb 100644 --- a/src/Arithmetic/BarrettReduction.v +++ b/src/Arithmetic/BarrettReduction.v @@ -101,7 +101,7 @@ Section Generic. rewrite xt_correct, q1_correct, q3_correct by auto with lia. assert (exists cond : bool, ((mu * (x / b^(k-1))) / b^(k+1)) = x / M + (if cond then -1 else 0)) as Hq3. { destruct q_nice_strong with (b:=b) (k:=k) (m:=mu) (offset:=1) (a:=x) (n:=M) as [cond Hcond]; - eauto using Z.lt_gt with zarith. } + eauto 2 using Z.lt_gt with zarith. } eauto using r_correct with lia. Qed. End Generic.