(* This file is autogenerated from Freeze.v by remake_packages.py *)
Require Import Crypto.Specific.Framework.CurveParametersPackage.
Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage.
Require Export Crypto.Specific.Framework.ArithmeticSynthesis.Freeze.
Require Import Crypto.Specific.Framework.Packages.
Require Import Crypto.Util.TagList.

Module TAG.
  Inductive tags := freeze_sig.
End TAG.

Ltac add_freeze_sig pkg :=
  Tag.update_by_tac_if_not_exists
    pkg
    TAG.freeze_sig
    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
                   let m := Tag.get pkg TAG.m in
                   let wt := Tag.get pkg TAG.wt in
                   let c := Tag.get pkg TAG.c in
                   let m_enc := Tag.get pkg TAG.m_enc in
                   let bitwidth := Tag.get pkg TAG.bitwidth in
                   let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
                   let wt_pos := Tag.get pkg TAG.wt_pos in
                   let wt_divides := Tag.get pkg TAG.wt_divides in
                   let wt_multiples := Tag.get pkg TAG.wt_multiples in
                   let freeze_sig := fresh "freeze_sig" in
                   let freeze_sig := pose_freeze_sig sz m wt c m_enc bitwidth wt_nonzero wt_pos wt_divides wt_multiples freeze_sig in
                   constr:(freeze_sig)).
Ltac add_Freeze_package pkg :=
  let pkg := add_freeze_sig pkg in
  Tag.strip_local pkg.


Module MakeFreezePackage (PKG : PrePackage).
  Module Import MakeFreezePackageInternal := MakePackageBase PKG.

  Ltac get_freeze_sig _ := get TAG.freeze_sig.
  Notation freeze_sig := (ltac:(let v := get_freeze_sig () in exact v)) (only parsing).
End MakeFreezePackage.