From a83d5122d26716268343491cdb4809e8a5f2a78e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 4 Dec 2018 16:17:09 -0500 Subject: Fix bugs introduced by previous commit --- src/Arithmetic/Saturated/Core.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Arithmetic') diff --git a/src/Arithmetic/Saturated/Core.v b/src/Arithmetic/Saturated/Core.v index 9c796ad57..a597b7bf2 100644 --- a/src/Arithmetic/Saturated/Core.v +++ b/src/Arithmetic/Saturated/Core.v @@ -398,7 +398,7 @@ Module Columns. Lemma map_sum_nils n : map sum (nils n) = B.Positional.zeros n. Proof using Type. cbv [nils B.Positional.zeros]; induction n as [|n]; [reflexivity|]. - change (repeat nil (S n)) with (@nil Z :: repeat nil n). + change (List.repeat nil (S n)) with (@nil Z :: List.repeat nil n). rewrite Tuple.map_repeat, sum_nil. reflexivity. Qed. -- cgit v1.2.3