diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-18 11:28:07 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-18 11:28:07 -0700 |
| commit | 6be6e0a4b9828512fda0d3d81cf56fdff808af27 (patch) | |
| tree | aed8405c6bc42497f219fbe483a9686c9eaae6d4 /src/Util/ListUtil.v | |
| parent | 15623b0cede2694310fc41a5802444e3e86ee35f (diff) | |
Fix some typos in the previous commit
Diffstat (limited to 'src/Util/ListUtil.v')
| -rw-r--r-- | src/Util/ListUtil.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index caeaefdb2..da02faa22 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -873,8 +873,8 @@ Proof. erewrite nth_error_value_eq_nth_default by eassumption; reflexivity. Qed. -Lemma nth_default_in_bounds : forall {T} n us (d d' : T), (n < length us)%nat -> - nth_default d us n = nth_default d us n. +Lemma nth_default_in_bounds : forall {T} (d' d : T) n us, (n < length us)%nat -> + nth_default d us n = nth_default d' us n. Proof. intros; erewrite !nth_default_nth_dep; reflexivity. Grab Existential Variables. |