diff options
| author |  Jason Gross <jagro@google.com> | 2016-08-12 10:15:03 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-08-12 10:15:03 -0700 |
| commit | 43d3a52cef9b0689ca4a557e7237db2c60875566 (patch) | |
| tree | b0211ecc8d71045a249a77e955a41124d89dded8 /src/ModularArithmetic/ModularBaseSystemProofs.v | |
| parent | 7483d6833d885498eff5cbb78f635ea914f921b5 (diff) | |
Fix build for Coq < 8.6
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemProofs.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 2331a0435..efc93a539 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -292,7 +292,7 @@ Section CarryProofs. Lemma carry_rep : forall i us x, (length us = length limb_widths)%nat -> - (i < length limb_widths)%nat -> + (i < length limb_widths)%nat -> forall pf1 pf2, from_list _ us pf1 ~= x -> from_list _ (carry i us) pf2 ~= x. Proof. @@ -332,7 +332,7 @@ Section CarryProofs. Qed. Opaque carry_full. - + Context `{cc : CarryChain limb_widths}. Lemma carry_mul_rep : forall us vs x y, rep us x -> rep vs y -> @@ -519,7 +519,7 @@ Section CanonicalizationProofs. fold (carry_sequence (make_chain i) us); rewrite length_carry_sequence; auto. repeat (break_if; try omega); try solve [rewrite Z.pow2_mod_spec by auto; autorewrite with zsimplify; apply Z.mod_pos_bound; zero_bounds]; - pose proof (IHi i us); pose proof (IHi n us); specialize_by assumption; specialize_by ltac:(auto with zarith); + pose proof (IHi i us); pose proof (IHi n us); specialize_by assumption; specialize_by auto with zarith; repeat break_if; try omega; pose proof c_pos; (split; try solve [zero_bounds]). (* TODO (jadep) : clean up/automate these leftover cases. *) - replace (2 * 2 ^ limb_widths [n]) with (2 ^ limb_widths [n] + 2 ^ limb_widths [n]) by ring. |