diff options
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 |