From ffc5e19d56b808e61fac1d94a9dfddc7b86cfa5d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 13:44:24 -0700 Subject: Fix for Coq 8.4 (missing lemmas) --- src/Util/ListUtil.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src') 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. -- cgit v1.2.3