From 24c557e38fac865e059832a17d6ae1591284bc42 Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Tue, 19 Jul 2016 16:41:20 -0700
Subject: Add a distr_length database

---
 src/Util/ListUtil.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src/Util')

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 :=
-- 
cgit v1.2.3