From aa1209f854d32463e96bb0d9cd30d40d0b7cb67c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 3 Oct 2017 15:48:41 -0400 Subject: Factor out some bits of ladderstep preglue This requires some changes to nonzero, which now needs to unfold proj1_sig itself. --- src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v | 1 + 1 file changed, 1 insertion(+) (limited to 'src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v') 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. -- cgit v1.2.3