diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-12-04 16:17:09 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-12-04 16:17:09 -0500 |
| commit | a83d5122d26716268343491cdb4809e8a5f2a78e (patch) | |
| tree | 147a990208e9611c02fe76683559028f496b2474 /src/Arithmetic | |
| parent | fe04d34c95b68bfa253631bfdfb61742e1bcf3b5 (diff) | |
Fix bugs introduced by previous commit
Diffstat (limited to 'src/Arithmetic')
| -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. |