(* 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.