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/ValueAnalysis.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'backend/ValueAnalysis.v') diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 7c4c0525..8aa4878a 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -875,7 +875,7 @@ Proof. apply smatch_ge with Nonstack. eapply SM. eapply mmatch_top; eauto. apply pge_lub_r. + (* below *) red; simpl; intros. destruct (eq_block b sp). - subst b. apply Plt_le_trans with bound. apply BELOW. congruence. auto. + subst b. apply Pos.lt_le_trans with bound. apply BELOW. congruence. auto. eapply mmatch_below; eauto. - (* genv *) eapply genv_match_exten; eauto. @@ -1008,7 +1008,7 @@ Proof. + apply SMTOP; auto. + apply SMTOP; auto. + red; simpl; intros. destruct (plt b (Mem.nextblock m)). - eapply Plt_le_trans. eauto. eapply external_call_nextblock; eauto. + eapply Pos.lt_le_trans. eauto. eapply external_call_nextblock; eauto. destruct (j' b) as [[bx deltax] | ] eqn:J'. eapply Mem.valid_block_inject_1; eauto. congruence. -- cgit