diff options
Diffstat (limited to 'src/Specific/Framework/SynthesisFramework.v')
-rw-r--r-- | src/Specific/Framework/SynthesisFramework.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/Specific/Framework/SynthesisFramework.v b/src/Specific/Framework/SynthesisFramework.v index c30024181..9c80efaa0 100644 --- a/src/Specific/Framework/SynthesisFramework.v +++ b/src/Specific/Framework/SynthesisFramework.v @@ -18,10 +18,14 @@ Module MakeSynthesisTactics (Curve : CurveParameters.CurveParameters). Ltac get_synthesis_package _ := let arithmetic_synthesis_pkg := AS.get_ArithmeticSynthesis_package () in lazymatch arithmetic_synthesis_pkg with - | (?sz, ?bitwidth, ?s, ?c, ?carry_chain1, ?carry_chain2, ?a24, ?coef_div_modulus, ?m, ?wt, ?sz2, ?m_enc, ?coef, ?coef_mod, ?sz_nonzero, ?wt_nonzero, ?wt_nonneg, ?wt_divides, ?wt_divides', ?wt_divides_chain1, ?wt_divides_chain2, ?zero_sig, ?one_sig, ?a24_sig, ?add_sig, ?sub_sig, ?opp_sig, ?mul_sig, ?square_sig, ?carry_sig, ?wt_pos, ?wt_multiples, ?freeze_sig, ?ring) + | (?sz, ?bitwidth, ?s, ?c, ?carry_chains, ?a24, ?coef_div_modulus, ?goldilocks, ?m, ?wt, ?sz2, ?m_enc, ?coef, ?coef_mod, ?sz_nonzero, ?wt_nonzero, ?wt_nonneg, ?wt_divides, ?wt_divides', ?wt_divides_chains, ?zero_sig, ?one_sig, ?a24_sig, ?add_sig, ?sub_sig, ?opp_sig, ?half_sz, ?half_sz_nonzero, ?sqrt_s, ?mul_sig, ?square_sig, ?carry_sig, ?wt_pos, ?wt_multiples, ?freeze_sig, ?ring) => let reification_types_pkg := get_ReificationTypes_package wt sz m wt_nonneg AS.P.upper_bound_of_exponent in let ladderstep_pkg := get_Ladderstep_package sz wt m add_sig sub_sig mul_sig square_sig carry_sig in constr:((arithmetic_synthesis_pkg, reification_types_pkg, ladderstep_pkg)) + | _ => let dummy := match goal with + | _ => fail "Did you update get_ArithmeticSynthesis_package but forget to update get_synthesis_package?" + end in + constr:(I : I) end. Ltac make_synthesis_package _ := lazymatch goal with |