diff options
Diffstat (limited to 'src/Arithmetic/Saturated/Core.v')
| -rw-r--r-- | src/Arithmetic/Saturated/Core.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |