From 25136fc8fa3162e3839b1f475e8aee699beb54d9 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre@roux01.fr>
Date: Mon, 14 Feb 2022 14:49:06 +0100
Subject: [PATCH] Require external libraries first

This way, an addition in external libraries
cannot shadow a definition in Prosa.
---
 analysis/abstract/abstract_rta.v                    | 4 ++--
 analysis/abstract/definitions.v                     | 2 +-
 analysis/abstract/ideal_jlfp_rta.v                  | 2 +-
 analysis/abstract/search_space.v                    | 2 +-
 analysis/definitions/carry_in.v                     | 2 +-
 analysis/definitions/hyperperiod.v                  | 2 +-
 analysis/facts/model/service_of_jobs.v              | 4 ++--
 analysis/facts/tdma.v                               | 2 +-
 analysis/facts/transform/wc_correctness.v           | 4 ++--
 behavior/job.v                                      | 2 +-
 model/priority/classes.v                            | 4 ++--
 model/schedule/tdma.v                               | 2 +-
 results/edf/rta/bounded_pi.v                        | 4 ++--
 results/edf/rta/floating_nonpreemptive.v            | 4 ++--
 results/edf/rta/fully_nonpreemptive.v               | 4 ++--
 results/edf/rta/fully_preemptive.v                  | 4 ++--
 results/edf/rta/limited_preemptive.v                | 4 ++--
 results/fifo/rta.v                                  | 4 ++--
 results/fixed_priority/rta/floating_nonpreemptive.v | 4 ++--
 results/fixed_priority/rta/fully_nonpreemptive.v    | 4 ++--
 results/fixed_priority/rta/fully_preemptive.v       | 4 ++--
 results/fixed_priority/rta/limited_preemptive.v     | 4 ++--
 util/div_mod.v                                      | 2 +-
 util/list.v                                         | 2 +-
 util/minmax.v                                       | 2 +-
 util/nat.v                                          | 2 +-
 util/nondecreasing.v                                | 2 +-
 util/sum.v                                          | 4 ++--
 util/unit_growth.v                                  | 2 +-
 29 files changed, 44 insertions(+), 44 deletions(-)

diff --git a/analysis/abstract/abstract_rta.v b/analysis/abstract/abstract_rta.v
index f3bfb0084..dae453703 100644
--- a/analysis/abstract/abstract_rta.v
+++ b/analysis/abstract/abstract_rta.v
@@ -1,9 +1,9 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
 Require Export prosa.analysis.definitions.schedulability.
 Require Export prosa.analysis.abstract.search_space.
 Require Export prosa.analysis.abstract.run_to_completion.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 (** * Abstract Response-Time Analysis *)
 (** In this module, we propose the general framework for response-time analysis (RTA) 
     of uni-processor scheduling of real-time tasks with arbitrary arrival models. *)
diff --git a/analysis/abstract/definitions.v b/analysis/abstract/definitions.v
index 461e4ef68..d37fabc71 100644
--- a/analysis/abstract/definitions.v
+++ b/analysis/abstract/definitions.v
@@ -1,5 +1,5 @@
-Require Export prosa.model.task.concept.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+Require Export prosa.model.task.concept.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import prosa.model.processor.ideal.  
diff --git a/analysis/abstract/ideal_jlfp_rta.v b/analysis/abstract/ideal_jlfp_rta.v
index c27b606f6..ef56378c5 100644
--- a/analysis/abstract/ideal_jlfp_rta.v
+++ b/analysis/abstract/ideal_jlfp_rta.v
@@ -1,6 +1,6 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 Require Export prosa.analysis.definitions.priority_inversion.
 Require Export prosa.analysis.abstract.abstract_seq_rta.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import prosa.model.processor.ideal.
diff --git a/analysis/abstract/search_space.v b/analysis/abstract/search_space.v
index 40b3d352e..ae74e993f 100644
--- a/analysis/abstract/search_space.v
+++ b/analysis/abstract/search_space.v
@@ -1,7 +1,7 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 Require Import prosa.util.epsilon.
 Require Import prosa.util.tactics.
 Require Import prosa.model.task.concept.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** * Reduction of the search space for Abstract RTA *)
 (** In this file, we prove that in order to calculate the worst-case response time 
diff --git a/analysis/definitions/carry_in.v b/analysis/definitions/carry_in.v
index f657e5bc2..b83bf9798 100644
--- a/analysis/definitions/carry_in.v
+++ b/analysis/definitions/carry_in.v
@@ -1,5 +1,5 @@
-Require Export prosa.model.priority.classes.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+Require Export prosa.model.priority.classes.
 
 (** * No Carry-In *)
 (** In this module, we define the notion of a time without any carry-in work. *)
diff --git a/analysis/definitions/hyperperiod.v b/analysis/definitions/hyperperiod.v
index 0d7bad8f6..a3754188b 100644
--- a/analysis/definitions/hyperperiod.v
+++ b/analysis/definitions/hyperperiod.v
@@ -1,6 +1,6 @@
+From mathcomp Require Import div.
 Require Export prosa.model.task.arrival.periodic.
 Require Export prosa.util.lcmseq.
-From mathcomp Require Import div.
 
 (** In this file we define the notion of a hyperperiod for periodic tasks. *)
 Section Hyperperiod.
diff --git a/analysis/facts/model/service_of_jobs.v b/analysis/facts/model/service_of_jobs.v
index 5670cd93d..5680f812e 100644
--- a/analysis/facts/model/service_of_jobs.v
+++ b/analysis/facts/model/service_of_jobs.v
@@ -1,11 +1,11 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
 Require Export prosa.model.aggregate.workload.
 Require Export prosa.model.aggregate.service_of_jobs.
 Require Export prosa.analysis.facts.behavior.completion.
 Require Export prosa.analysis.facts.model.ideal_schedule.
 Require Import prosa.model.processor.ideal.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
-
 (** * Lemmas about Service Received by Sets of Jobs *)
 (** In this file, we establish basic facts about the service received by _sets_ of jobs. *)
 
diff --git a/analysis/facts/tdma.v b/analysis/facts/tdma.v
index a94adcd6a..aca8b5cc0 100644
--- a/analysis/facts/tdma.v
+++ b/analysis/facts/tdma.v
@@ -1,6 +1,6 @@
+From mathcomp Require Import div.
 Require Export prosa.model.schedule.tdma.
 Require Import prosa.util.all.
-From mathcomp Require Import div.
 
 (** In this section, we define the properties of TDMA and prove some basic lemmas. *)
 Section TDMAFacts.
diff --git a/analysis/facts/transform/wc_correctness.v b/analysis/facts/transform/wc_correctness.v
index 2042cb138..c9cdd027b 100644
--- a/analysis/facts/transform/wc_correctness.v
+++ b/analysis/facts/transform/wc_correctness.v
@@ -1,3 +1,5 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
 Require Export prosa.model.schedule.work_conserving.
 Require Export prosa.analysis.facts.model.ideal_schedule.
 Require Export prosa.analysis.transform.wc_trans.
@@ -5,8 +7,6 @@ Require Export prosa.analysis.facts.transform.swaps.
 Require Export prosa.analysis.definitions.schedulability.
 Require Export prosa.util.list.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
-
 (** * Correctness of the work-conservation transformation *)
 (** This file contains the main argument of the work-conservation proof,
     starting with an analysis of the individual functions that drive
diff --git a/behavior/job.v b/behavior/job.v
index e5d17882b..d008c8219 100644
--- a/behavior/job.v
+++ b/behavior/job.v
@@ -1,5 +1,5 @@
-Require Export prosa.behavior.time.
 From mathcomp Require Export eqtype ssrnat.
+Require Export prosa.behavior.time.
 
 (** * Notion of a Job Type *)
 
diff --git a/model/priority/classes.v b/model/priority/classes.v
index 8646455a9..ac48795dc 100644
--- a/model/priority/classes.v
+++ b/model/priority/classes.v
@@ -1,9 +1,9 @@
+From mathcomp Require Export seq.
+
 Require Export prosa.model.task.concept.
 Require Export prosa.util.rel.
 Require Export prosa.util.list.
 
-From mathcomp Require Export seq.
-
 (** * The FP, JLFP, and JLDP Priority Classes *)
 
 (** In this module, we define the three well-known classes of priority
diff --git a/model/schedule/tdma.v b/model/schedule/tdma.v
index 47a79907c..68f5fd46f 100644
--- a/model/schedule/tdma.v
+++ b/model/schedule/tdma.v
@@ -1,7 +1,7 @@
+From mathcomp Require Import div.
 Require Export prosa.model.task.concept.
 Require Export prosa.util.seqset.
 Require Export prosa.util.rel.
-From mathcomp Require Import div.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require prosa.model.processor.ideal.
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index bf82c7bf6..88113de4f 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -1,3 +1,5 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
 Require Export prosa.analysis.facts.priority.edf.
 Require Export prosa.analysis.definitions.schedulability.
 Require Import prosa.model.priority.edf.
@@ -6,8 +8,6 @@ Require Import prosa.analysis.abstract.ideal_jlfp_rta.
 Require Import prosa.analysis.facts.busy_interval.carry_in.
 Require Import prosa.analysis.facts.readiness.basic.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 (** Throughout this file, we assume ideal uni-processor schedules ... *)
 Require Import prosa.model.processor.ideal.
 
diff --git a/results/edf/rta/floating_nonpreemptive.v b/results/edf/rta/floating_nonpreemptive.v
index c6f3cde84..9859fc710 100644
--- a/results/edf/rta/floating_nonpreemptive.v
+++ b/results/edf/rta/floating_nonpreemptive.v
@@ -1,9 +1,9 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
 Require Export prosa.results.edf.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.floating.
 Require Export prosa.analysis.facts.readiness.sequential.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 (** * RTA for EDF with Floating Non-Preemptive Regions *)
 (** In this module we prove the RTA theorem for floating non-preemptive regions EDF model. *)
 
diff --git a/results/edf/rta/fully_nonpreemptive.v b/results/edf/rta/fully_nonpreemptive.v
index 4034a3e6e..8f9fbe80d 100644
--- a/results/edf/rta/fully_nonpreemptive.v
+++ b/results/edf/rta/fully_nonpreemptive.v
@@ -1,10 +1,10 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
 Require Export prosa.results.edf.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.task.nonpreemptive.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive.
 Require Export prosa.analysis.facts.readiness.basic.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 
 (** * RTA for Fully Non-Preemptive EDF *)
 (** In this module we prove the RTA theorem for the fully non-preemptive EDF model. *)
diff --git a/results/edf/rta/fully_preemptive.v b/results/edf/rta/fully_preemptive.v
index 5ca06a9c0..e3a339584 100644
--- a/results/edf/rta/fully_preemptive.v
+++ b/results/edf/rta/fully_preemptive.v
@@ -1,10 +1,10 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
 Require Import prosa.results.edf.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.task.preemptive.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.preemptive.
 Require Export prosa.analysis.facts.readiness.basic.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 (** * RTA for Fully Preemptive EDF *)
 (** In this section we prove the RTA theorem for the fully preemptive EDF model *)
 
diff --git a/results/edf/rta/limited_preemptive.v b/results/edf/rta/limited_preemptive.v
index cbfced66a..309dfbeff 100644
--- a/results/edf/rta/limited_preemptive.v
+++ b/results/edf/rta/limited_preemptive.v
@@ -1,9 +1,9 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
 Require Export prosa.results.edf.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.limited.
 Require Export prosa.analysis.facts.readiness.basic.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 (** * RTA for EDF with Fixed Preemption Points *)
 (** In this module we prove the RTA theorem for EDF-schedulers with
     fixed preemption points. *)
diff --git a/results/fifo/rta.v b/results/fifo/rta.v
index 1a2f653be..f0d99bc85 100644
--- a/results/fifo/rta.v
+++ b/results/fifo/rta.v
@@ -1,10 +1,10 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
 Require Import prosa.analysis.facts.priority.fifo. 
 Require Import prosa.model.priority.fifo.
 Require Import prosa.analysis.abstract.ideal_jlfp_rta.
 Require Export prosa.analysis.facts.busy_interval.carry_in.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 (** Throughout this file, we assume ideal uni-processor schedules ... *)
 Require Import prosa.model.processor.ideal.
 
diff --git a/results/fixed_priority/rta/floating_nonpreemptive.v b/results/fixed_priority/rta/floating_nonpreemptive.v
index f7d9c99f0..469954409 100644
--- a/results/fixed_priority/rta/floating_nonpreemptive.v
+++ b/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -1,9 +1,9 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
 Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.floating.
 Require Export prosa.analysis.facts.readiness.sequential.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 
 (** * RTA for Model with Floating Non-Preemptive Regions *)
 (** In this module we prove the RTA theorem for floating non-preemptive regions FP model. *)
diff --git a/results/fixed_priority/rta/fully_nonpreemptive.v b/results/fixed_priority/rta/fully_nonpreemptive.v
index 5de85eaf4..3191a4e00 100644
--- a/results/fixed_priority/rta/fully_nonpreemptive.v
+++ b/results/fixed_priority/rta/fully_nonpreemptive.v
@@ -1,10 +1,10 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
 Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.task.nonpreemptive.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive.
 Require Export prosa.analysis.facts.readiness.sequential.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 
 (** * RTA for Fully Non-Preemptive FP Model *)
 (** In this module we prove the RTA theorem for the fully non-preemptive FP model. *)
diff --git a/results/fixed_priority/rta/fully_preemptive.v b/results/fixed_priority/rta/fully_preemptive.v
index 7e2b4800a..28ceef67f 100644
--- a/results/fixed_priority/rta/fully_preemptive.v
+++ b/results/fixed_priority/rta/fully_preemptive.v
@@ -1,10 +1,10 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
 Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.task.preemptive.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.preemptive.
 Require Export prosa.analysis.facts.readiness.sequential.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 
 (** * RTA for Fully Preemptive FP Model *)
 (** In this section we prove the RTA theorem for the fully preemptive FP model *)
diff --git a/results/fixed_priority/rta/limited_preemptive.v b/results/fixed_priority/rta/limited_preemptive.v
index 14de81fb1..ff425f254 100644
--- a/results/fixed_priority/rta/limited_preemptive.v
+++ b/results/fixed_priority/rta/limited_preemptive.v
@@ -1,9 +1,9 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
 Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.limited.
 Require Export prosa.analysis.facts.readiness.sequential.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 
 (** * RTA for FP-schedulers with Fixed Preemption Points *)
 (** In this module we prove the RTA theorem for FP-schedulers with
diff --git a/util/div_mod.v b/util/div_mod.v
index e82386c7c..eed01ed2b 100644
--- a/util/div_mod.v
+++ b/util/div_mod.v
@@ -1,5 +1,5 @@
-Require Export prosa.util.nat prosa.util.subadditivity.
 From mathcomp Require Export ssreflect ssrbool eqtype ssrnat seq fintype bigop div ssrfun.
+Require Export prosa.util.nat prosa.util.subadditivity.
 
 (** Additional lemmas about [divn] and [modn]. *)
 Section DivMod.
diff --git a/util/list.v b/util/list.v
index 006559beb..ebceb3a85 100644
--- a/util/list.v
+++ b/util/list.v
@@ -1,6 +1,6 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 Require Import prosa.util.ssrlia prosa.util.tactics.
 Require Export prosa.util.supremum.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** We define a few simple operations on lists that return zero for
     empty lists: [max0], [first0], and [last0]. *)
diff --git a/util/minmax.v b/util/minmax.v
index 736d5cdc5..be2ad47ad 100644
--- a/util/minmax.v
+++ b/util/minmax.v
@@ -1,5 +1,5 @@
-Require Export prosa.util.notation prosa.util.nat prosa.util.list.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+Require Export prosa.util.notation prosa.util.nat prosa.util.list.
 
 (** Additional lemmas about [BigMax]. *)
 Section ExtraLemmas.
diff --git a/util/nat.v b/util/nat.v
index 9bf128120..f32799344 100644
--- a/util/nat.v
+++ b/util/nat.v
@@ -1,5 +1,5 @@
-Require Export prosa.util.tactics prosa.util.ssrlia.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
+Require Export prosa.util.tactics prosa.util.ssrlia.
 
 (** Additional lemmas about natural numbers. *)
 Section NatLemmas.
diff --git a/util/nondecreasing.v b/util/nondecreasing.v
index 2a890adf4..f55b3c7b8 100644
--- a/util/nondecreasing.v
+++ b/util/nondecreasing.v
@@ -1,7 +1,7 @@
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 Require Export prosa.util.epsilon.
 Require Export prosa.util.nat.
 Require Export prosa.util.list.
-From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 (** * Non-Decreasing Sequence and Distances *)
 (** In this file we introduce the notion of a non-decreasing sequence. *)
diff --git a/util/sum.v b/util/sum.v
index 47a3209ee..febadac56 100644
--- a/util/sum.v
+++ b/util/sum.v
@@ -1,8 +1,8 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
+
 Require Export prosa.util.notation.
 Require Export prosa.util.nat.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
-
 Section SumsOverSequences.
 
   (** Consider any type [I] with a decidable equality ... *)
diff --git a/util/unit_growth.v b/util/unit_growth.v
index d29f82ac1..cb75e30f4 100644
--- a/util/unit_growth.v
+++ b/util/unit_growth.v
@@ -1,5 +1,5 @@
-Require Import prosa.util.tactics prosa.util.notation.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat.
+Require Import prosa.util.tactics prosa.util.notation.
 
 (** We say that a function [f] is a unit growth function iff for any
     time instant [t] it holds that [f (t + 1) <= f t + 1]. *)
-- 
GitLab