From a4baa73fe061ae8f948b8cf9a887668d05061855 Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Tue, 17 Apr 2018 13:28:08 +0200 Subject: fix the placement of a dlet to make more sense --- src/Experiments/SimplyTypedArithmetic.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index bafe666e4..a8f1e0a13 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -1284,7 +1284,7 @@ Module Rows. fold_right (fun next (state : list Z * Z * nat) => let i := snd state in let low_high' := - dlet_nd low_high := fst state in + let low_high := fst state in let low := fst low_high in let high := snd low_high in dlet_nd sum_carry := Z.add_with_get_carry_full (fw i) high (fst next) (snd next) in -- cgit v1.2.3