diff options
author | Jason Gross <jagro@google.com> | 2016-07-18 13:44:24 -0700 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2016-07-18 13:44:24 -0700 |
commit | ffc5e19d56b808e61fac1d94a9dfddc7b86cfa5d (patch) | |
tree | df01607ca0adfe524778d7aa38a827283e6a9662 /src/Util | |
parent | dc585913d86991a12826e181a66f9c3a02afbd8f (diff) |
Fix for Coq 8.4 (missing lemmas)
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 da02faa22..3006dd799 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -854,21 +854,21 @@ Proof. | Some v => fun _ => v | None => fun bad => match _ : False with end end eq_refl). - apply (proj1 (@List.nth_error_None _ _ _)) in bad; generalize dependent (length ls); clear. + apply (proj1 (@nth_error_None _ _ _)) in bad; instantiate; generalize dependent (length ls); clear. abstract (intros; omega). Defined. Lemma nth_error_nth_dep {A} ls n pf : nth_error ls n = Some (@nth_dep A ls n pf). Proof. unfold nth_dep. - generalize dependent (List.nth_error_None ls n). + generalize dependent (@nth_error_None A ls n). edestruct nth_error; boring. Qed. Lemma nth_default_nth_dep {A} d ls n pf : nth_default d ls n = @nth_dep A ls n pf. Proof. unfold nth_dep. - generalize dependent (List.nth_error_None ls n). + generalize dependent (@nth_error_None A ls n). destruct (nth_error ls n) eqn:?; boring. erewrite nth_error_value_eq_nth_default by eassumption; reflexivity. Qed. |