diff options
| author |  Jason Gross <jagro@google.com> | 2016-08-16 17:32:02 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-08-16 17:33:31 -0700 |
| commit | 73802f7713b2b4ed3a2c386048c3bcb838a8da7e (patch) | |
| tree | eb4cd2ec46c61551e5bc2a21aa0e827fbaaa94b3 /src/ModularArithmetic/Pow2BaseProofs.v | |
| parent | db3c7f74189786dd644928a82a48f21cf887c8c7 (diff) | |
Fixes for Coq 8.4
Diffstat (limited to 'src/ModularArithmetic/Pow2BaseProofs.v')
| -rw-r--r-- | src/ModularArithmetic/Pow2BaseProofs.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 631e3a970..8a1de034a 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -390,7 +390,7 @@ Section Pow2BaseProofs. replace (map (fun x => two_p zero * (two_p w * x)) (base_from_limb_widths limb_widths')) with (map (Z.mul (two_p (zero + w))) (base_from_limb_widths limb_widths')) by (apply map_ext; rewrite two_p_is_exp by auto with zarith omega; auto with zarith). change 0 with (0 + 0) at 1. - apply Z.add_le_mono; auto with zarith. + apply Z.add_le_mono; simpl in *; auto with zarith. Qed. Lemma decode_upper_bound : forall us, @@ -1571,7 +1571,7 @@ Section carrying. Proof. unfold carry_simple; intros; rewrite carry_gen_decode_eq by assumption. autorewrite with natsimplify. - break_match; lia. + break_match; try lia; autorewrite with zsimplify; lia. Qed. |