From 760f02864acd20c30cfd3df54f85fb080bf9ea0d Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Mon, 19 Feb 2018 11:02:36 +0100 Subject: Fix naming issue --- 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 16e53ad33..189e76113 100644 --- a/src/Arithmetic/Saturated/Core.v +++ b/src/Arithmetic/Saturated/Core.v @@ -394,7 +394,7 @@ Module Columns. Proof using Type. cbv [nils B.Positional.zeros]; induction n as [|n]; [reflexivity|]. change (repeat nil (S n)) with (@nil Z :: repeat nil n). - rewrite map_repeat, sum_nil. reflexivity. + rewrite Tuple.map_repeat, sum_nil. reflexivity. Qed. Lemma eval_nils n : eval (nils n) = 0. -- cgit v1.2.3