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. --- riscV/Conventions1.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'riscV/Conventions1.v') diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v index ff993650..df7ddfd2 100644 --- a/riscV/Conventions1.v +++ b/riscV/Conventions1.v @@ -420,7 +420,7 @@ Proof. ofs + typesize ty <= max_outgoing_2 n p). { intros. destruct p; simpl in H; intuition; subst; simpl. - xomega. - - eapply Zle_trans. 2: apply A. xomega. + - eapply Z.le_trans. 2: apply A. xomega. - xomega. } assert (C: forall l n, In (S Outgoing ofs ty) (regs_of_rpairs l) -> @@ -428,7 +428,7 @@ Proof. { induction l; simpl; intros. - contradiction. - rewrite in_app_iff in H. destruct H. - + eapply Zle_trans. eapply B; eauto. apply Zge_le. apply fold_max_outgoing_above. + + eapply Z.le_trans. eapply B; eauto. apply Z.ge_le. apply fold_max_outgoing_above. + apply IHl; auto. } apply C. -- cgit