diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-07-10 01:33:42 -0700 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-07-10 01:33:42 -0700 |
| commit | 649d3e8730703d47068418c312f33550b8709695 (patch) | |
| tree | 058d45d9e3e2cf5399796df378dc2bbc362d6fad /src/Util/ListUtil.v | |
| parent | ec9916567173178cf710481e5715bca2be40f81a (diff) | |
Fix ListUtil for Coq 8.4
Diffstat (limited to 'src/Util/ListUtil.v')
| -rw-r--r-- | src/Util/ListUtil.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |