diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-09-22 19:50:52 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-09-22 19:53:06 +0200 |
| commit | 8d5c6bb8f0cac1339dec7b730997ee30b1517073 (patch) | |
| tree | 3ffd8bcb28a88ae4ff51989aed37b0ad2cb676b2 /backend/CSEproof.v | |
| parent | 0f210f622a4609811959f4450f770c61f5eb6532 (diff) | |
| download | compcert-kvx-8d5c6bb8f0cac1339dec7b730997ee30b1517073.tar.gz compcert-kvx-8d5c6bb8f0cac1339dec7b730997ee30b1517073.zip | |
Remove coq warnings (#28)
Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
Diffstat (limited to 'backend/CSEproof.v')
| -rw-r--r-- | backend/CSEproof.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 8516e384..d6bde348 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -35,8 +35,8 @@ Remark wf_equation_incr: wf_equation next1 e -> Ple next1 next2 -> wf_equation next2 e. Proof. unfold wf_equation; intros; destruct e. destruct H. split. - apply Plt_le_trans with next1; auto. - red; intros. apply Plt_le_trans with next1; auto. apply H1; auto. + apply Pos.lt_le_trans with next1; auto. + red; intros. apply Pos.lt_le_trans with next1; auto. apply H1; auto. Qed. (** Extensionality with respect to valuations. *) @@ -95,7 +95,7 @@ Proof. - auto. - apply equation_holds_exten. auto. eapply wf_equation_incr; eauto with cse. -- rewrite AGREE. eauto. eapply Plt_le_trans; eauto. eapply wf_num_reg; eauto. +- rewrite AGREE. eauto. eapply Pos.lt_le_trans; eauto. eapply wf_num_reg; eauto. Qed. End EXTEN. @@ -523,7 +523,7 @@ Proof. exists valu3. constructor; simpl; intros. + constructor; simpl; intros; eauto with cse. destruct H4; eauto with cse. subst e. split. - eapply Plt_le_trans; eauto. + eapply Pos.lt_le_trans; eauto. red; simpl; intros. auto. + destruct H4; eauto with cse. subst eq. apply eq_holds_lessdef with (Val.load_result chunk rs#src). apply load_eval_to with a. rewrite <- Q; auto. @@ -1187,7 +1187,7 @@ Proof. - (* internal function *) monadInv TFD. unfold transf_function in EQ. fold (analyze cu f) in EQ. destruct (analyze cu f) as [approx|] eqn:?; inv EQ. - exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_extends; eauto. apply Z.le_refl. apply Z.le_refl. intros (m'' & A & B). econstructor; split. eapply exec_function_internal; simpl; eauto. |