diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-03 15:48:41 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-10-05 13:34:14 -0400 |
| commit | aa1209f854d32463e96bb0d9cd30d40d0b7cb67c (patch) | |
| tree | 334cd146aafc6f8c063ed7b9fdea7b922277c62e /src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v | |
| parent | 96fa708e46d304ce4594983f8914bb01cc21b87a (diff) | |
Factor out some bits of ladderstep preglue
This requires some changes to nonzero, which now needs to unfold
proj1_sig itself.
Diffstat (limited to 'src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v')
| -rw-r--r-- | src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v b/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v index 3c605e348..27e710fe6 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v @@ -80,6 +80,7 @@ Section BoundedField25p5. cbv_runtime. reflexivity. sig_dlet_in_rhs_to_context. + cbv [proj1_sig]. match goal with | [ H : feBW_small |- _ ] => destruct H as [? _] end. |