diff options
Diffstat (limited to 'src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v')
| -rw-r--r-- | src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v | 498 |
1 files changed, 0 insertions, 498 deletions
diff --git a/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v b/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v deleted file mode 100644 index cefc0733f..000000000 --- a/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v +++ /dev/null @@ -1,498 +0,0 @@ -(* This file is autogenerated from Montgomery.v by remake_packages.py *) -Require Import Crypto.Specific.Framework.CurveParametersPackage. -Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage. -Require Import Crypto.Specific.Framework.ArithmeticSynthesis.DefaultsPackage. -Require Import Crypto.Specific.Framework.ArithmeticSynthesis.FreezePackage. -Require Import Crypto.Specific.Framework.ArithmeticSynthesis.LadderstepPackage. -Require Export Crypto.Specific.Framework.ArithmeticSynthesis.Montgomery. -Require Import Crypto.Specific.Framework.Packages. -Require Import Crypto.Util.TagList. - -Module TAG. - Inductive tags := m' | r' | m'_correct | r'_correct | m_enc_correct_montgomery | r'_pow_correct | montgomery_to_F | r_big | m_big | m_enc_small | map_m_enc | mul_ext | add_ext | sub_ext | opp_ext | carry_ext | nonzero_ext | mul_bounded | add_bounded | sub_bounded | opp_bounded | carry_bounded | nonzero_sig. -End TAG. - -Ltac add_m' pkg := - if_montgomery - pkg - ltac:(fun _ => let modinv_fuel := Tag.get pkg TAG.modinv_fuel in - let m := Tag.get pkg TAG.m in - let r := Tag.get pkg TAG.r in - let m' := fresh "m'" in - let m' := pose_m' modinv_fuel m r m' in - Tag.update pkg TAG.m' m') - ltac:(fun _ => pkg) - (). -Ltac add_r' pkg := - if_montgomery - pkg - ltac:(fun _ => let modinv_fuel := Tag.get pkg TAG.modinv_fuel in - let m := Tag.get pkg TAG.m in - let r := Tag.get pkg TAG.r in - let r' := fresh "r'" in - let r' := pose_r' modinv_fuel m r r' in - Tag.update pkg TAG.r' r') - ltac:(fun _ => pkg) - (). -Ltac add_m'_correct pkg := - if_montgomery - pkg - ltac:(fun _ => let m := Tag.get pkg TAG.m in - let m' := Tag.get pkg TAG.m' in - let r := Tag.get pkg TAG.r in - let m'_correct := fresh "m'_correct" in - let m'_correct := pose_m'_correct m m' r m'_correct in - Tag.update pkg TAG.m'_correct m'_correct) - ltac:(fun _ => pkg) - (). -Ltac add_r'_correct pkg := - if_montgomery - pkg - ltac:(fun _ => let m := Tag.get pkg TAG.m in - let r := Tag.get pkg TAG.r in - let r' := Tag.get pkg TAG.r' in - let r'_correct := fresh "r'_correct" in - let r'_correct := pose_r'_correct m r r' r'_correct in - Tag.update pkg TAG.r'_correct r'_correct) - ltac:(fun _ => pkg) - (). -Ltac add_m_enc_correct_montgomery pkg := - if_montgomery - pkg - ltac:(fun _ => let m := Tag.get pkg TAG.m in - let sz := Tag.get pkg TAG.sz in - let r := Tag.get pkg TAG.r in - let m_enc := Tag.get pkg TAG.m_enc in - let m_enc_correct_montgomery := fresh "m_enc_correct_montgomery" in - let m_enc_correct_montgomery := pose_m_enc_correct_montgomery m sz r m_enc m_enc_correct_montgomery in - Tag.update pkg TAG.m_enc_correct_montgomery m_enc_correct_montgomery) - ltac:(fun _ => pkg) - (). -Ltac add_r'_pow_correct pkg := - if_montgomery - pkg - ltac:(fun _ => let r' := Tag.get pkg TAG.r' in - let sz := Tag.get pkg TAG.sz in - let r := Tag.get pkg TAG.r in - let m_enc := Tag.get pkg TAG.m_enc in - let r'_pow_correct := fresh "r'_pow_correct" in - let r'_pow_correct := pose_r'_pow_correct r' sz r m_enc r'_pow_correct in - Tag.update pkg TAG.r'_pow_correct r'_pow_correct) - ltac:(fun _ => pkg) - (). -Ltac add_montgomery_to_F pkg := - if_montgomery - pkg - ltac:(fun _ => let sz := Tag.get pkg TAG.sz in - let m := Tag.get pkg TAG.m in - let r' := Tag.get pkg TAG.r' in - let montgomery_to_F := fresh "montgomery_to_F" in - let montgomery_to_F := pose_montgomery_to_F sz m r' montgomery_to_F in - Tag.update pkg TAG.montgomery_to_F montgomery_to_F) - ltac:(fun _ => pkg) - (). -Ltac add_r_big pkg := - if_montgomery - pkg - ltac:(fun _ => let r := Tag.get pkg TAG.r in - let r_big := fresh "r_big" in - let r_big := pose_r_big r r_big in - Tag.update pkg TAG.r_big r_big) - ltac:(fun _ => pkg) - (). -Ltac add_m_big pkg := - if_montgomery - pkg - ltac:(fun _ => let m := Tag.get pkg TAG.m in - let m_big := fresh "m_big" in - let m_big := pose_m_big m m_big in - Tag.update pkg TAG.m_big m_big) - ltac:(fun _ => pkg) - (). -Ltac add_m_enc_small pkg := - if_montgomery - pkg - ltac:(fun _ => let sz := Tag.get pkg TAG.sz in - let r := Tag.get pkg TAG.r in - let m_enc := Tag.get pkg TAG.m_enc in - let m_enc_small := fresh "m_enc_small" in - let m_enc_small := pose_m_enc_small sz r m_enc m_enc_small in - Tag.update pkg TAG.m_enc_small m_enc_small) - ltac:(fun _ => pkg) - (). -Ltac add_map_m_enc pkg := - if_montgomery - pkg - ltac:(fun _ => let sz := Tag.get pkg TAG.sz in - let r := Tag.get pkg TAG.r in - let m_enc := Tag.get pkg TAG.m_enc in - let map_m_enc := fresh "map_m_enc" in - let map_m_enc := pose_map_m_enc sz r m_enc map_m_enc in - Tag.update pkg TAG.map_m_enc map_m_enc) - ltac:(fun _ => pkg) - (). -Ltac add_mul_ext pkg := - if_montgomery - pkg - ltac:(fun _ => let r := Tag.get pkg TAG.r in - let sz := Tag.get pkg TAG.sz in - let m := Tag.get pkg TAG.m in - let m_enc := Tag.get pkg TAG.m_enc in - let r' := Tag.get pkg TAG.r' in - let r'_correct := Tag.get pkg TAG.r'_correct in - let m' := Tag.get pkg TAG.m' in - let m'_correct := Tag.get pkg TAG.m'_correct in - let m_enc_correct_montgomery := Tag.get pkg TAG.m_enc_correct_montgomery in - let r_big := Tag.get pkg TAG.r_big in - let m_big := Tag.get pkg TAG.m_big in - let m_enc_small := Tag.get pkg TAG.m_enc_small in - let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in - let mul_ext := fresh "mul_ext" in - let mul_ext := pose_mul_ext r sz m m_enc r' r'_correct m' m'_correct m_enc_correct_montgomery r_big m_big m_enc_small montgomery_to_F mul_ext in - Tag.update pkg TAG.mul_ext mul_ext) - ltac:(fun _ => pkg) - (). -Ltac add_add_ext pkg := - if_montgomery - pkg - ltac:(fun _ => let r := Tag.get pkg TAG.r in - let sz := Tag.get pkg TAG.sz in - let m := Tag.get pkg TAG.m in - let m_enc := Tag.get pkg TAG.m_enc in - let r' := Tag.get pkg TAG.r' in - let m_enc_correct_montgomery := Tag.get pkg TAG.m_enc_correct_montgomery in - let r_big := Tag.get pkg TAG.r_big in - let m_big := Tag.get pkg TAG.m_big in - let m_enc_small := Tag.get pkg TAG.m_enc_small in - let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in - let add_ext := fresh "add_ext" in - let add_ext := pose_add_ext r sz m m_enc r' m_enc_correct_montgomery r_big m_big m_enc_small montgomery_to_F add_ext in - Tag.update pkg TAG.add_ext add_ext) - ltac:(fun _ => pkg) - (). -Ltac add_sub_ext pkg := - if_montgomery - pkg - ltac:(fun _ => let r := Tag.get pkg TAG.r in - let sz := Tag.get pkg TAG.sz in - let m := Tag.get pkg TAG.m in - let m_enc := Tag.get pkg TAG.m_enc in - let r' := Tag.get pkg TAG.r' in - let m_enc_correct_montgomery := Tag.get pkg TAG.m_enc_correct_montgomery in - let r_big := Tag.get pkg TAG.r_big in - let m_enc_small := Tag.get pkg TAG.m_enc_small in - let map_m_enc := Tag.get pkg TAG.map_m_enc in - let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in - let sub_ext := fresh "sub_ext" in - let sub_ext := pose_sub_ext r sz m m_enc r' m_enc_correct_montgomery r_big m_enc_small map_m_enc montgomery_to_F sub_ext in - Tag.update pkg TAG.sub_ext sub_ext) - ltac:(fun _ => pkg) - (). -Ltac add_opp_ext pkg := - if_montgomery - pkg - ltac:(fun _ => let r := Tag.get pkg TAG.r in - let sz := Tag.get pkg TAG.sz in - let m := Tag.get pkg TAG.m in - let m_enc := Tag.get pkg TAG.m_enc in - let r' := Tag.get pkg TAG.r' in - let m_enc_correct_montgomery := Tag.get pkg TAG.m_enc_correct_montgomery in - let r_big := Tag.get pkg TAG.r_big in - let m_enc_small := Tag.get pkg TAG.m_enc_small in - let map_m_enc := Tag.get pkg TAG.map_m_enc in - let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in - let opp_ext := fresh "opp_ext" in - let opp_ext := pose_opp_ext r sz m m_enc r' m_enc_correct_montgomery r_big m_enc_small map_m_enc montgomery_to_F opp_ext in - Tag.update pkg TAG.opp_ext opp_ext) - ltac:(fun _ => pkg) - (). -Ltac add_carry_ext pkg := - if_montgomery - pkg - ltac:(fun _ => let r := Tag.get pkg TAG.r in - let sz := Tag.get pkg TAG.sz in - let m := Tag.get pkg TAG.m in - let m_enc := Tag.get pkg TAG.m_enc in - let r' := Tag.get pkg TAG.r' in - let r_big := Tag.get pkg TAG.r_big in - let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in - let carry_ext := fresh "carry_ext" in - let carry_ext := pose_carry_ext r sz m m_enc r' r_big montgomery_to_F carry_ext in - Tag.update pkg TAG.carry_ext carry_ext) - ltac:(fun _ => pkg) - (). -Ltac add_nonzero_ext pkg := - if_montgomery - pkg - ltac:(fun _ => let r := Tag.get pkg TAG.r in - let sz := Tag.get pkg TAG.sz in - let m := Tag.get pkg TAG.m in - let m_enc := Tag.get pkg TAG.m_enc in - let r' := Tag.get pkg TAG.r' in - let m_enc_correct_montgomery := Tag.get pkg TAG.m_enc_correct_montgomery in - let r'_pow_correct := Tag.get pkg TAG.r'_pow_correct in - let r_big := Tag.get pkg TAG.r_big in - let m_big := Tag.get pkg TAG.m_big in - let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in - let nonzero_ext := fresh "nonzero_ext" in - let nonzero_ext := pose_nonzero_ext r sz m m_enc r' m_enc_correct_montgomery r'_pow_correct r_big m_big montgomery_to_F nonzero_ext in - Tag.update pkg TAG.nonzero_ext nonzero_ext) - ltac:(fun _ => pkg) - (). -Ltac add_mul_sig pkg := - if_montgomery - pkg - ltac:(fun _ => let r := Tag.get pkg TAG.r in - let sz := Tag.get pkg TAG.sz in - let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in - let mul_ext := Tag.get pkg TAG.mul_ext in - let mul_sig := fresh "mul_sig" in - let mul_sig := pose_mul_sig r sz montgomery_to_F mul_ext mul_sig in - Tag.update pkg TAG.mul_sig mul_sig) - ltac:(fun _ => pkg) - (). -Ltac add_mul_bounded pkg := - if_montgomery - pkg - ltac:(fun _ => let r := Tag.get pkg TAG.r in - let sz := Tag.get pkg TAG.sz in - let m_enc := Tag.get pkg TAG.m_enc in - let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in - let mul_ext := Tag.get pkg TAG.mul_ext in - let mul_sig := Tag.get pkg TAG.mul_sig in - let mul_bounded := fresh "mul_bounded" in - let mul_bounded := pose_mul_bounded r sz m_enc montgomery_to_F mul_ext mul_sig mul_bounded in - Tag.update pkg TAG.mul_bounded mul_bounded) - ltac:(fun _ => pkg) - (). -Ltac add_add_sig pkg := - if_montgomery - pkg - ltac:(fun _ => let r := Tag.get pkg TAG.r in - let sz := Tag.get pkg TAG.sz in - let m_enc := Tag.get pkg TAG.m_enc in - let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in - let add_ext := Tag.get pkg TAG.add_ext in - let add_sig := fresh "add_sig" in - let add_sig := pose_add_sig r sz m_enc montgomery_to_F add_ext add_sig in - Tag.update pkg TAG.add_sig add_sig) - ltac:(fun _ => pkg) - (). -Ltac add_add_bounded pkg := - if_montgomery - pkg - ltac:(fun _ => let r := Tag.get pkg TAG.r in - let sz := Tag.get pkg TAG.sz in - let m_enc := Tag.get pkg TAG.m_enc in - let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in - let add_ext := Tag.get pkg TAG.add_ext in - let add_sig := Tag.get pkg TAG.add_sig in - let add_bounded := fresh "add_bounded" in - let add_bounded := pose_add_bounded r sz m_enc montgomery_to_F add_ext add_sig add_bounded in - Tag.update pkg TAG.add_bounded add_bounded) - ltac:(fun _ => pkg) - (). -Ltac add_sub_sig pkg := - if_montgomery - pkg - ltac:(fun _ => let r := Tag.get pkg TAG.r in - let sz := Tag.get pkg TAG.sz in - let m_enc := Tag.get pkg TAG.m_enc in - let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in - let sub_ext := Tag.get pkg TAG.sub_ext in - let sub_sig := fresh "sub_sig" in - let sub_sig := pose_sub_sig r sz m_enc montgomery_to_F sub_ext sub_sig in - Tag.update pkg TAG.sub_sig sub_sig) - ltac:(fun _ => pkg) - (). -Ltac add_sub_bounded pkg := - if_montgomery - pkg - ltac:(fun _ => let r := Tag.get pkg TAG.r in - let sz := Tag.get pkg TAG.sz in - let m_enc := Tag.get pkg TAG.m_enc in - let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in - let sub_ext := Tag.get pkg TAG.sub_ext in - let sub_sig := Tag.get pkg TAG.sub_sig in - let sub_bounded := fresh "sub_bounded" in - let sub_bounded := pose_sub_bounded r sz m_enc montgomery_to_F sub_ext sub_sig sub_bounded in - Tag.update pkg TAG.sub_bounded sub_bounded) - ltac:(fun _ => pkg) - (). -Ltac add_opp_sig pkg := - if_montgomery - pkg - ltac:(fun _ => let r := Tag.get pkg TAG.r in - let sz := Tag.get pkg TAG.sz in - let m_enc := Tag.get pkg TAG.m_enc in - let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in - let opp_ext := Tag.get pkg TAG.opp_ext in - let opp_sig := fresh "opp_sig" in - let opp_sig := pose_opp_sig r sz m_enc montgomery_to_F opp_ext opp_sig in - Tag.update pkg TAG.opp_sig opp_sig) - ltac:(fun _ => pkg) - (). -Ltac add_opp_bounded pkg := - if_montgomery - pkg - ltac:(fun _ => let r := Tag.get pkg TAG.r in - let sz := Tag.get pkg TAG.sz in - let m_enc := Tag.get pkg TAG.m_enc in - let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in - let opp_ext := Tag.get pkg TAG.opp_ext in - let opp_sig := Tag.get pkg TAG.opp_sig in - let opp_bounded := fresh "opp_bounded" in - let opp_bounded := pose_opp_bounded r sz m_enc montgomery_to_F opp_ext opp_sig opp_bounded in - Tag.update pkg TAG.opp_bounded opp_bounded) - ltac:(fun _ => pkg) - (). -Ltac add_carry_sig pkg := - if_montgomery - pkg - ltac:(fun _ => let r := Tag.get pkg TAG.r in - let sz := Tag.get pkg TAG.sz in - let m_enc := Tag.get pkg TAG.m_enc in - let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in - let carry_ext := Tag.get pkg TAG.carry_ext in - let carry_sig := fresh "carry_sig" in - let carry_sig := pose_carry_sig r sz m_enc montgomery_to_F carry_ext carry_sig in - Tag.update pkg TAG.carry_sig carry_sig) - ltac:(fun _ => pkg) - (). -Ltac add_carry_bounded pkg := - if_montgomery - pkg - ltac:(fun _ => let r := Tag.get pkg TAG.r in - let sz := Tag.get pkg TAG.sz in - let m_enc := Tag.get pkg TAG.m_enc in - let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in - let carry_ext := Tag.get pkg TAG.carry_ext in - let carry_sig := Tag.get pkg TAG.carry_sig in - let carry_bounded := fresh "carry_bounded" in - let carry_bounded := pose_carry_bounded r sz m_enc montgomery_to_F carry_ext carry_sig carry_bounded in - Tag.update pkg TAG.carry_bounded carry_bounded) - ltac:(fun _ => pkg) - (). -Ltac add_nonzero_sig pkg := - if_montgomery - pkg - ltac:(fun _ => let r := Tag.get pkg TAG.r in - let sz := Tag.get pkg TAG.sz in - let m := Tag.get pkg TAG.m in - let m_enc := Tag.get pkg TAG.m_enc in - let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in - let nonzero_ext := Tag.get pkg TAG.nonzero_ext in - let nonzero_sig := fresh "nonzero_sig" in - let nonzero_sig := pose_nonzero_sig r sz m m_enc montgomery_to_F nonzero_ext nonzero_sig in - Tag.update pkg TAG.nonzero_sig nonzero_sig) - ltac:(fun _ => pkg) - (). -Ltac add_ring pkg := - if_montgomery - pkg - ltac:(fun _ => let ring := fresh "ring" in - let ring := pose_ring ring in - Tag.update pkg TAG.ring ring) - ltac:(fun _ => pkg) - (). -Ltac add_freeze_sig pkg := - if_montgomery - pkg - ltac:(fun _ => let freeze_sig := fresh "freeze_sig" in - let freeze_sig := pose_freeze_sig freeze_sig in - Tag.update pkg TAG.freeze_sig freeze_sig) - ltac:(fun _ => pkg) - (). -Ltac add_Mxzladderstep_sig pkg := - if_montgomery - pkg - ltac:(fun _ => let Mxzladderstep_sig := fresh "Mxzladderstep_sig" in - let Mxzladderstep_sig := pose_Mxzladderstep_sig Mxzladderstep_sig in - Tag.update pkg TAG.Mxzladderstep_sig Mxzladderstep_sig) - ltac:(fun _ => pkg) - (). -Ltac add_Montgomery_package pkg := - let pkg := add_m' pkg in - let pkg := add_r' pkg in - let pkg := add_m'_correct pkg in - let pkg := add_r'_correct pkg in - let pkg := add_m_enc_correct_montgomery pkg in - let pkg := add_r'_pow_correct pkg in - let pkg := add_montgomery_to_F pkg in - let pkg := add_r_big pkg in - let pkg := add_m_big pkg in - let pkg := add_m_enc_small pkg in - let pkg := add_map_m_enc pkg in - let pkg := add_mul_ext pkg in - let pkg := add_add_ext pkg in - let pkg := add_sub_ext pkg in - let pkg := add_opp_ext pkg in - let pkg := add_carry_ext pkg in - let pkg := add_nonzero_ext pkg in - let pkg := add_mul_sig pkg in - let pkg := add_mul_bounded pkg in - let pkg := add_add_sig pkg in - let pkg := add_add_bounded pkg in - let pkg := add_sub_sig pkg in - let pkg := add_sub_bounded pkg in - let pkg := add_opp_sig pkg in - let pkg := add_opp_bounded pkg in - let pkg := add_carry_sig pkg in - let pkg := add_carry_bounded pkg in - let pkg := add_nonzero_sig pkg in - let pkg := add_ring pkg in - let pkg := add_freeze_sig pkg in - let pkg := add_Mxzladderstep_sig pkg in - Tag.strip_subst_local pkg. - - -Module MakeMontgomeryPackage (PKG : PrePackage). - Module Import MakeMontgomeryPackageInternal := MakePackageBase PKG. - - Ltac get_m' _ := get TAG.m'. - Notation m' := (ltac:(let v := get_m' () in exact v)) (only parsing). - Ltac get_r' _ := get TAG.r'. - Notation r' := (ltac:(let v := get_r' () in exact v)) (only parsing). - Ltac get_m'_correct _ := get TAG.m'_correct. - Notation m'_correct := (ltac:(let v := get_m'_correct () in exact v)) (only parsing). - Ltac get_r'_correct _ := get TAG.r'_correct. - Notation r'_correct := (ltac:(let v := get_r'_correct () in exact v)) (only parsing). - Ltac get_m_enc_correct_montgomery _ := get TAG.m_enc_correct_montgomery. - Notation m_enc_correct_montgomery := (ltac:(let v := get_m_enc_correct_montgomery () in exact v)) (only parsing). - Ltac get_r'_pow_correct _ := get TAG.r'_pow_correct. - Notation r'_pow_correct := (ltac:(let v := get_r'_pow_correct () in exact v)) (only parsing). - Ltac get_montgomery_to_F _ := get TAG.montgomery_to_F. - Notation montgomery_to_F := (ltac:(let v := get_montgomery_to_F () in exact v)) (only parsing). - Ltac get_r_big _ := get TAG.r_big. - Notation r_big := (ltac:(let v := get_r_big () in exact v)) (only parsing). - Ltac get_m_big _ := get TAG.m_big. - Notation m_big := (ltac:(let v := get_m_big () in exact v)) (only parsing). - Ltac get_m_enc_small _ := get TAG.m_enc_small. - Notation m_enc_small := (ltac:(let v := get_m_enc_small () in exact v)) (only parsing). - Ltac get_map_m_enc _ := get TAG.map_m_enc. - Notation map_m_enc := (ltac:(let v := get_map_m_enc () in exact v)) (only parsing). - Ltac get_mul_ext _ := get TAG.mul_ext. - Notation mul_ext := (ltac:(let v := get_mul_ext () in exact v)) (only parsing). - Ltac get_add_ext _ := get TAG.add_ext. - Notation add_ext := (ltac:(let v := get_add_ext () in exact v)) (only parsing). - Ltac get_sub_ext _ := get TAG.sub_ext. - Notation sub_ext := (ltac:(let v := get_sub_ext () in exact v)) (only parsing). - Ltac get_opp_ext _ := get TAG.opp_ext. - Notation opp_ext := (ltac:(let v := get_opp_ext () in exact v)) (only parsing). - Ltac get_carry_ext _ := get TAG.carry_ext. - Notation carry_ext := (ltac:(let v := get_carry_ext () in exact v)) (only parsing). - Ltac get_nonzero_ext _ := get TAG.nonzero_ext. - Notation nonzero_ext := (ltac:(let v := get_nonzero_ext () in exact v)) (only parsing). - Ltac get_mul_bounded _ := get TAG.mul_bounded. - Notation mul_bounded := (ltac:(let v := get_mul_bounded () in exact v)) (only parsing). - Ltac get_add_bounded _ := get TAG.add_bounded. - Notation add_bounded := (ltac:(let v := get_add_bounded () in exact v)) (only parsing). - Ltac get_sub_bounded _ := get TAG.sub_bounded. - Notation sub_bounded := (ltac:(let v := get_sub_bounded () in exact v)) (only parsing). - Ltac get_opp_bounded _ := get TAG.opp_bounded. - Notation opp_bounded := (ltac:(let v := get_opp_bounded () in exact v)) (only parsing). - Ltac get_carry_bounded _ := get TAG.carry_bounded. - Notation carry_bounded := (ltac:(let v := get_carry_bounded () in exact v)) (only parsing). - Ltac get_nonzero_sig _ := get TAG.nonzero_sig. - Notation nonzero_sig := (ltac:(let v := get_nonzero_sig () in exact v)) (only parsing). -End MakeMontgomeryPackage. |