diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-07-08 10:29:49 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-07-08 10:29:49 -0400 |
| commit | 72fd2095b56a6d39eb53c837aaf0098290a3dda7 (patch) | |
| tree | 1a280c971bba58890629a47f9eb4930fc88f6ec2 /src/Util | |
| parent | 2b4f574fe712d5f8af1bcbb8689188d56e19b3c2 (diff) | |
Fix ListUtil for Coq 8.4
[rewrite_strat] ignores [using tac] sometimes, and [Hint Rewrite] only
accepts one database in 8.4.
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/ListUtil.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 483cd4417..705407836 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -981,7 +981,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. reflexivity. + (rewrite_strat topdown hints simpl_nth_default); eauto using eq_refl with nocore. Qed. Hint Rewrite @sum_firstn_succ using congruence : simpl_sum_firstn. @@ -1068,5 +1068,7 @@ Proof. congruence. Qed. -Hint Rewrite @firstn_update_nth : push_firstn pull_update_nth. -Hint Rewrite <- @firstn_update_nth : pull_firstn push_update_nth. +Hint Rewrite @firstn_update_nth : push_firstn. +Hint Rewrite @firstn_update_nth : pull_update_nth. +Hint Rewrite <- @firstn_update_nth : pull_firstn. +Hint Rewrite <- @firstn_update_nth : push_update_nth. |