Deduplicate some code

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))