diff options
| -rw-r--r-- | src/Util/ListUtil.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 8b92ef4fa..1032e1dc2 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -38,6 +38,8 @@ Hint Rewrite @prod_length : distr_length. +Hint Extern 1 => progress autorewrite with distr_length in * : distr_length. + Definition sum_firstn l n := fold_right Z.add 0%Z (firstn n l). Fixpoint map2 {A B C} (f : A -> B -> C) (la : list A) (lb : list B) : list C := |