diff options
author | 2016-11-14 22:37:11 -0500 | |
---|---|---|
committer | 2016-11-14 22:37:11 -0500 | |
commit | 740d9168a8dd6de27398446447f95043d93defaa (patch) | |
tree | 989fe7c455980f8cb3514334c381d86b25f89b9a /src/SpecificGen/GF41417_32BoundedCommon.v | |
parent | cf94b28c80f3c3b89f0ac39c33aad9c703af56d0 (diff) |
Copy over better prefreeze
Diffstat (limited to 'src/SpecificGen/GF41417_32BoundedCommon.v')
-rw-r--r-- | src/SpecificGen/GF41417_32BoundedCommon.v | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/src/SpecificGen/GF41417_32BoundedCommon.v b/src/SpecificGen/GF41417_32BoundedCommon.v index fec786e23..92a90bd16 100644 --- a/src/SpecificGen/GF41417_32BoundedCommon.v +++ b/src/SpecificGen/GF41417_32BoundedCommon.v @@ -300,14 +300,19 @@ Ltac unfold_is_bounded_in' H := unfold_is_bounded_in' H2 | _ => idtac end. -Ltac unfold_is_bounded_in H := +Ltac preunfold_is_bounded_in H := unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe41417_32WToZ, wire_digitsWToZ in H; - cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe41417_32 List.length wire_widths] in H; + cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe41417_32 List.length wire_widths] in H. +Ltac unfold_is_bounded_in H := + preunfold_is_bounded_in H; unfold_is_bounded_in' H. -Ltac unfold_is_bounded := +Ltac preunfold_is_bounded := unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe41417_32WToZ, wire_digitsWToZ; - cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe41417_32 List.length wire_widths]; + cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe41417_32 List.length wire_widths]. + +Ltac unfold_is_bounded := + preunfold_is_bounded; repeat match goal with | [ |- andb _ _ = true ] => apply andb_true_intro | [ |- and _ _ ] => split |