From 26faf65015eb8d6a9ce57772feb05c7dc63a1dea Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 6 Nov 2017 12:57:04 -0500 Subject: Deduplicate some code --- src/Util/CPSUtil.v | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'src/Util/CPSUtil.v') 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)) -- cgit v1.2.3