From 649d3e8730703d47068418c312f33550b8709695 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 10 Jul 2016 01:33:42 -0700 Subject: Fix ListUtil for Coq 8.4 --- src/Util/ListUtil.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 3b08c52c4..9931fb9b1 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1022,7 +1022,7 @@ Lemma sum_firstn_succ : forall l i x, sum_firstn l (S i) = (x + sum_firstn l i)%Z. Proof. intros; rewrite sum_firstn_succ_default. - (rewrite_strat topdown hints simpl_nth_default); eauto using eq_refl with nocore. + erewrite nth_error_value_eq_nth_default by eassumption; reflexivity. Qed. Hint Rewrite @sum_firstn_succ using congruence : simpl_sum_firstn. -- cgit v1.2.3