aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/Framework/ReificationTypesPackage.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Specific/Framework/ReificationTypesPackage.v')
-rw-r--r--src/Specific/Framework/ReificationTypesPackage.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Specific/Framework/ReificationTypesPackage.v b/src/Specific/Framework/ReificationTypesPackage.v
index 4a868856e..2a5e8e85b 100644
--- a/src/Specific/Framework/ReificationTypesPackage.v
+++ b/src/Specific/Framework/ReificationTypesPackage.v
@@ -38,9 +38,9 @@ Ltac add_bound1 pkg :=
Tag.update pkg TAG.bound1 bound1.
Ltac add_lgbitwidth pkg :=
- let limb_widths := Tag.get pkg TAG.limb_widths in
+ let bitwidth := Tag.get pkg TAG.bitwidth in
let lgbitwidth := fresh "lgbitwidth" in
- let lgbitwidth := pose_local_lgbitwidth limb_widths lgbitwidth in
+ let lgbitwidth := pose_local_lgbitwidth bitwidth lgbitwidth in
Tag.local_update pkg TAG.lgbitwidth lgbitwidth.
Ltac add_adjusted_bitwidth' pkg :=