diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-16 15:39:20 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-16 15:39:20 -0400 |
| commit | c2cfdbede87ffb0489384fe41365961fbd4d1df8 (patch) | |
| tree | 1b5f8efca74ceaac004cca37144d5a56fa77f4e6 /src | |
| parent | dd9a8741e316de351e12727431f09135597c169d (diff) | |
Fix build
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. |