diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-10-06 11:59:06 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-10-06 11:59:06 -0400 |
| commit | 6d27149299a6aaaca3d82480c1b0e90a98cc18a7 (patch) | |
| tree | dc587b6a65b937c11e4bcdb2c9c8df3a26b630f8 /src/Specific/GF25519.v | |
| parent | f2c6c26737e97e539d09945cd0b429971bc8b09b (diff) | |
Moved conversion logic out of Pow2BaseProofs into its own file
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index d98781f9f..ebaa54080 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -457,7 +457,7 @@ Proof. eexists. cbv [pack_opt]. repeat (rewrite <-convert'_opt_correct; - cbv - [from_list_default_opt Pow2BaseProofs.convert']). + cbv - [from_list_default_opt Conversion.convert']). repeat progress rewrite ?Z.shiftl_0_r, ?Z.shiftr_0_r, ?Z.land_0_l, ?Z.lor_0_l, ?Z.land_same_r. cbv [from_list_default_opt]. reflexivity. @@ -503,7 +503,7 @@ Proof. cbv [unpack_opt]. repeat ( rewrite <-convert'_opt_correct; - cbv - [from_list_default_opt Pow2BaseProofs.convert']). + cbv - [from_list_default_opt Conversion.convert']). repeat progress rewrite ?Z.shiftl_0_r, ?Z.shiftr_0_r, ?Z.land_0_l, ?Z.lor_0_l, ?Z.land_same_r. cbv [from_list_default_opt]. reflexivity. |