From 6f8121d538d128da4bf167696cd8632b1df537cf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Mon, 26 Jul 2021 11:39:52 +0200
Subject: [PATCH] address deprecation warnings (iota_add -> iotaD)
mathcomp has deprecated `iota_add` in favor of `iotaD`.
However, `iotaD` wasn't added until mathcomp 1.12, so this patch breaks
compatibility with earlier versions.
---
.../facts/preemption/rtc_threshold/job_preemptable.v | 6 +++---
util/nondecreasing.v | 11 +++++------
2 files changed, 8 insertions(+), 9 deletions(-)
diff --git a/analysis/facts/preemption/rtc_threshold/job_preemptable.v b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
index 269cf6477..8dba9cc61 100644
--- a/analysis/facts/preemption/rtc_threshold/job_preemptable.v
+++ b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
@@ -71,7 +71,7 @@ Section RunToCompletionThreshold.
Proof.
intros POS.
unfold job_preemption_points, range, index_iota; rewrite subn0 -addn1.
- rewrite iota_add add0n filter_cat mem_cat.
+ rewrite iotaD add0n filter_cat mem_cat.
apply/orP; right; simpl.
destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.
unfold job_cannot_be_nonpreemptive_after_completion in *.
@@ -111,9 +111,9 @@ Section RunToCompletionThreshold.
erewrite last0_filter.
+ by apply/eqP; apply eq_refl.
+ unfold range, index_iota; rewrite subn0 -addn1.
- by rewrite iota_add; destruct (iota 0 (job_cost j)).
+ by rewrite iotaD; destruct (iota 0 (job_cost j)).
+ unfold range, index_iota; rewrite subn0 -addn1.
- by rewrite iota_add last0_cat //.
+ by rewrite iotaD last0_cat //.
+ by apply A2.
Qed.
diff --git a/util/nondecreasing.v b/util/nondecreasing.v
index 1462134ca..2a890adf4 100644
--- a/util/nondecreasing.v
+++ b/util/nondecreasing.v
@@ -583,20 +583,19 @@ Section NondecreasingSequence.
Qed.
(** We prove that [index_iota 0 n] produces a sequence of numbers
- which are always one unit apart each other. *)
+ which are always one unit apart from each other. *)
Lemma distances_of_iota_ε:
forall n x, x \in distances (index_iota 0 n) -> x = ε.
Proof.
intros n x IN; induction n.
- by unfold index_iota, distances in IN.
- destruct n; first by unfold distances, index_iota in IN.
- rewrite -addn1 /index_iota subn0 iota_add in IN.
- rewrite add0n in IN.
- rewrite distances_unfold_1app_last in IN; last by rewrite size_iota.
- move: IN; rewrite mem_cat; move => /orP [IN|IN].
+ move: IN; rewrite -addn1 /index_iota subn0 iotaD add0n.
+ rewrite distances_unfold_1app_last; last by rewrite size_iota.
+ rewrite mem_cat => /orP [IN|IN].
+ by apply IHn; rewrite /index_iota subn0; simpl.
+ by move: IN;
- rewrite -addn1 iota_add /last0 last_cat add0n addn1 // subSnn in_cons;
+ rewrite -addn1 iotaD /last0 last_cat add0n addn1 // subSnn in_cons;
move => /orP [/eqP EQ|F]; subst.
Qed.
--
GitLab