diff options
Diffstat (limited to 'src/Util/CPSUtil.v')
| -rw-r--r-- | src/Util/CPSUtil.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/Util/CPSUtil.v b/src/Util/CPSUtil.v index fc7d43b93..927d071f6 100644 --- a/src/Util/CPSUtil.v +++ b/src/Util/CPSUtil.v @@ -115,14 +115,12 @@ Definition id_tuple'_with_alt_cps {R A n} (value value_for_alt : forall R, (Tuple.tuple' A n -> R) -> R) (f : Tuple.tuple' A n -> R) : R - := dlet z := id_tuple'_with_alt (value _ id) (value_for_alt _ id) in - f z. + := id_tuple'_with_alt_cps' (value _) (value_for_alt _) f. Definition id_tuple_with_alt_cps {R A n} (value value_for_alt : forall R, (Tuple.tuple A n -> R) -> R) (f : Tuple.tuple A n -> R) : R - := dlet z := id_tuple_with_alt (value _ id) (value_for_alt _ id) in - f z. + := id_tuple_with_alt_cps' (value _) (value_for_alt _) f. Definition id_tuple'_with_alt_cps_correct {R A n} value value_for_alt f : @id_tuple'_with_alt_cps R A n value value_for_alt f = f (id_tuple'_with_alt (value _ id) (value_for_alt _ id)) |