diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-07 14:24:24 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-07 14:24:24 -0700 |
| commit | bd2fcf4e05bc6fd389be917fa52dcbfe08af5ec0 (patch) | |
| tree | e6fac9862cdf7499de5cbe1d7836d4a6965f7fd7 /src/Util | |
| parent | ad60847a0217cb55e477b9e5a750e480588a67da (diff) | |
Correct hintdb names
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/ListUtil.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index dbc6797c7..fd592e3b9 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -929,7 +929,7 @@ Proof. congruence. Qed. -Hint Rewrite @sum_firstn_all_succ using omega : simpl_firstn. +Hint Rewrite @sum_firstn_all_succ using omega : simpl_sum_firstn. Lemma sum_firstn_succ_default : forall l i, sum_firstn l (S i) = (nth_default 0 l i + sum_firstn l i)%Z. @@ -940,7 +940,7 @@ Proof. rewrite IHl; omega. Qed. -Hint Rewrite @sum_firstn_succ_default : simpl_firstn. +Hint Rewrite @sum_firstn_succ_default : simpl_sum_firstn. Lemma sum_firstn_succ : forall l i x, nth_error l i = Some x -> @@ -950,7 +950,7 @@ Proof. rewrite_strat topdown hints simpl_nth_default. reflexivity. Qed. -Hint Rewrite @sum_firstn_succ using congruence : simpl_firstn. +Hint Rewrite @sum_firstn_succ using congruence : simpl_sum_firstn. Lemma nth_default_map2 : forall {A B C} (f : A -> B -> C) ls1 ls2 i d d1 d2, nth_default d (map2 f ls1 ls2) i = |