diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-20 13:47:58 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-20 13:52:18 -0400 |
| commit | 5d0b83966f5a31ddbe2ff35e21ea967bfb5a2d3d (patch) | |
| tree | a777742a5f554e2c570cf8a75da934e79de95af4 /src/Specific/MontgomeryP256_128.v | |
| parent | 6f7cb2dc6acc4e0aa00c80e550879ee36d35e6a4 (diff) | |
Make use of new conditional_subtract
Diffstat (limited to 'src/Specific/MontgomeryP256_128.v')
| -rw-r--r-- | src/Specific/MontgomeryP256_128.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Specific/MontgomeryP256_128.v b/src/Specific/MontgomeryP256_128.v index 503c97572..1136f394f 100644 --- a/src/Specific/MontgomeryP256_128.v +++ b/src/Specific/MontgomeryP256_128.v @@ -28,7 +28,7 @@ Definition mulmod_256' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple }. Proof. eapply (lift2_sig (fun A B c => c = _)); eexists. - cbv -[Definitions.Z.add_get_carry Definitions.Z.mul_split_at_bitwidth runtime_add runtime_mul Let_In]. + cbv -[Definitions.Z.add_get_carry Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. (* cbv [ r wt sz p256 |