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 /lib/Iteration.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 'lib/Iteration.v')
| -rw-r--r-- | lib/Iteration.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/Iteration.v b/lib/Iteration.v index 4398f96d..6a9d3253 100644 --- a/lib/Iteration.v +++ b/lib/Iteration.v @@ -146,7 +146,7 @@ Definition iter_step (x: positive) | right NOTEQ => match step s with | inl res => Some res - | inr s' => next (Ppred x) (Ppred_Plt x NOTEQ) s' + | inr s' => next (Pos.pred x) (Ppred_Plt x NOTEQ) s' end end. @@ -176,7 +176,7 @@ Proof. specialize (step_prop a H0). destruct (step a) as [b'|a'] eqn:?. inv H1. auto. - apply H with (Ppred x) a'. apply Ppred_Plt; auto. auto. auto. + apply H with (Pos.pred x) a'. apply Ppred_Plt; auto. auto. auto. Qed. Lemma iterate_prop: |