diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-06 12:45:50 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-06 12:45:50 -0500 |
| commit | 3d3e0331434281be95fc35ef8d141f61f57d9f32 (patch) | |
| tree | d54a8c969d6093c47aa2a382e674a9ad2668ee16 /src/Arithmetic/Core.v | |
| parent | 52a84764eadd3e673869c2cd1d868a7809e55871 (diff) | |
Make use of id_tuple_with_alt_cps'
Diffstat (limited to 'src/Arithmetic/Core.v')
| -rw-r--r-- | src/Arithmetic/Core.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v index 4293561fa..929aa2260 100644 --- a/src/Arithmetic/Core.v +++ b/src/Arithmetic/Core.v @@ -1076,7 +1076,7 @@ Hint Unfold Positional.select_cps Positional.select modulo div modulo_cps div_cps - id_tuple_with_alt id_tuple'_with_alt + id_tuple_with_alt id_tuple'_with_alt id_tuple_with_alt_cps' Z.add_get_carry_full Z.add_get_carry_full_cps : basesystem_partial_evaluation_unfolder. @@ -1084,7 +1084,7 @@ Hint Unfold B.limb ListUtil.sum ListUtil.sum_firstn CPSUtil.Tuple.mapi_with_cps CPSUtil.Tuple.mapi_with'_cps CPSUtil.flat_map_cps CPSUtil.on_tuple_cps CPSUtil.fold_right_cps2 Decidable.dec Decidable.dec_eq_Z - id_tuple_with_alt id_tuple'_with_alt + id_tuple_with_alt id_tuple'_with_alt id_tuple_with_alt_cps' Z.add_get_carry_full Z.add_get_carry_full_cps Z.mul_split Z.mul_split_cps Z.mul_split_cps' : basesystem_partial_evaluation_unfolder. @@ -1110,7 +1110,7 @@ Ltac basesystem_partial_evaluation_unfolder t := Associational.carryterm_cps Associational.carryterm Associational.carry_cps Associational.carry Associational.negate_snd_cps Associational.negate_snd div modulo - id_tuple_with_alt id_tuple'_with_alt + id_tuple_with_alt id_tuple'_with_alt id_tuple_with_alt_cps' Z.add_get_carry_full Z.add_get_carry_full_cps ] in t. |