diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Specific/MontgomreyP256.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/Specific/MontgomreyP256.v b/src/Specific/MontgomreyP256.v index fd328dae3..9db230ac4 100644 --- a/src/Specific/MontgomreyP256.v +++ b/src/Specific/MontgomreyP256.v @@ -34,7 +34,7 @@ Proof. Positional.to_associational_cps Saturated.divmod_cps Saturated.scmul_cps - Saturated.uweight + Saturated.uweight Saturated.Columns.mul_cps Saturated.Associational.mul_cps Z.of_nat Pos.of_succ_nat Nat.pred @@ -54,7 +54,7 @@ Tuple.tuple *) (* CPSUtil.to_list_cps CPSUtil.to_list'_cps CPSUtil.to_list_cps' Positional.zeros -Tuple.to_list +Tuple.to_list Tuple.to_list' List.hd List.tl @@ -67,4 +67,5 @@ Z.of_nat *) cbv [List.app]. (* cbv -[runtime_add runtime_mul LetIn.Let_In Definitions.Z.add_get_carry_full Definitions.Z.mul_split]. *) - (* basesystem_partial_evaluation_RHS. *)
\ No newline at end of file + (* basesystem_partial_evaluation_RHS. *) +Abort. |