From 8d5c6bb8f0cac1339dec7b730997ee30b1517073 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 22 Sep 2017 19:50:52 +0200 Subject: Remove coq warnings (#28) Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts. --- backend/Selectionproof.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'backend/Selectionproof.v') diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index ebc64c6f..86d7ff21 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -209,7 +209,7 @@ Lemma eval_load: Proof. intros. generalize H0; destruct v; simpl; intro; try discriminate. unfold load. - generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (refl_equal _)). + generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (eq_refl _)). destruct (addressing chunk a). intros [vl [EV EQ]]. eapply eval_Eload; eauto. Qed. @@ -224,7 +224,7 @@ Lemma eval_store: Proof. intros. generalize H1; destruct v1; simpl; intro; try discriminate. unfold store. - generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (refl_equal _)). + generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (eq_refl _)). destruct (addressing chunk a1). intros [vl [EV EQ]]. eapply step_store; eauto. Qed. @@ -1036,7 +1036,7 @@ Proof. - (* internal function *) destruct TF as (hf & HF & TF). specialize (MC cunit hf). monadInv TF. generalize EQ; intros TF; monadInv TF. - exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl. intros [m2' [A B]]. left; econstructor; split. econstructor; simpl; eauto. -- cgit