From ba8dc43be5a0b6008830b0d64811a5217949a8ac Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Sat, 23 Nov 2019 15:42:41 +0100
Subject: [PATCH] Don't Export modules that introduce new Instances

---
 .../analysis/basic_facts/preemption/job/limited.v          | 2 +-
 .../analysis/edf/rta/nonpr_reg/concrete_models/floating.v  | 2 ++
 .../analysis/edf/rta/nonpr_reg/concrete_models/limited.v   | 2 ++
 .../edf/rta/nonpr_reg/concrete_models/nonpreemptive.v      | 1 +
 .../edf/rta/nonpr_reg/concrete_models/preemptive.v         | 1 +
 .../analysis/edf/rta/nonpr_reg/response_time_bound.v       | 1 +
 restructuring/analysis/edf/rta/response_time_bound.v       | 2 ++
 restructuring/analysis/facts/edf.v                         | 4 ++--
 .../analysis/facts/priority_inversion_is_bounded.v         | 3 +++
 restructuring/analysis/facts/readiness/basic.v             | 4 +++-
 .../rta/nonpr_reg/concrete_models/floating.v               | 1 +
 .../fixed_priority/rta/nonpr_reg/concrete_models/limited.v | 1 +
 restructuring/analysis/schedulability.v                    | 2 +-
 restructuring/model/schedule/limited_preemptive.v          | 7 ++++---
 restructuring/model/schedule/preemption_time.v             | 4 +++-
 restructuring/model/schedule/tdma.v                        | 4 +++-
 restructuring/model/task/preemption/limited_preemptive.v   | 4 ++--
 17 files changed, 33 insertions(+), 12 deletions(-)

diff --git a/restructuring/analysis/basic_facts/preemption/job/limited.v b/restructuring/analysis/basic_facts/preemption/job/limited.v
index 81e57d575..392482c93 100644
--- a/restructuring/analysis/basic_facts/preemption/job/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/job/limited.v
@@ -2,7 +2,7 @@ Require Export rt.restructuring.analysis.basic_facts.all.
 Require Export rt.restructuring.analysis.definitions.job_properties.
 Require Export rt.restructuring.model.schedule.limited_preemptive.
 
-Require Export rt.restructuring.model.preemption.limited_preemptive.
+Require Import rt.restructuring.model.preemption.limited_preemptive.
 
 (** * Platform for Models with Limited Preemptions *)
 (** In this section, we prove that instantiation of predicate
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
index 1d05d354e..0fd62e5c4 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
@@ -1,8 +1,10 @@
 Require Export rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating.
+Require Import rt.restructuring.model.priority.edf.
 
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
index 5f3aafd52..b7550071d 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
@@ -1,8 +1,10 @@
 Require Export rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited.
+Require Import rt.restructuring.model.priority.edf.
 
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.limited_preemptive.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
index 503ea76a0..725cc69ac 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
@@ -4,6 +4,7 @@ Require Import rt.restructuring.model.readiness.basic.
 Require Export rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
 Require Export rt.restructuring.analysis.basic_facts.preemption.task.nonpreemptive.
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive.
+Require Import rt.restructuring.model.priority.edf.
 
 (** Assume we have a fully non-preemptive model. *)
 Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
index 338deb120..6197685dc 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
@@ -4,6 +4,7 @@ Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
 Require Export rt.restructuring.analysis.basic_facts.preemption.task.preemptive.
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.preemptive.
+Require Import rt.restructuring.model.priority.edf.
 
 (** Assume we have a fully preemptive model. *)
 Require Import rt.restructuring.model.task.preemption.fully_preemptive.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
index de5919d64..885eb5881 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
@@ -1,6 +1,7 @@
 Require Export rt.restructuring.analysis.facts.priority_inversion_is_bounded.
 Require Export rt.restructuring.analysis.edf.rta.response_time_bound.
 Require Export rt.restructuring.analysis.arrival.rbf.
+Require Import rt.restructuring.model.priority.edf.
 
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
diff --git a/restructuring/analysis/edf/rta/response_time_bound.v b/restructuring/analysis/edf/rta/response_time_bound.v
index 5d71602be..982e050af 100644
--- a/restructuring/analysis/edf/rta/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/response_time_bound.v
@@ -2,6 +2,8 @@ Require Export rt.restructuring.analysis.facts.edf.
 Require Export rt.restructuring.model.schedule.priority_driven.
 Require Export rt.restructuring.analysis.facts.no_carry_in_exists.
 Require Export rt.restructuring.analysis.schedulability.
+Require Import rt.restructuring.model.priority.edf.
+Require Import rt.restructuring.model.task.absolute_deadline.
 
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
diff --git a/restructuring/analysis/facts/edf.v b/restructuring/analysis/facts/edf.v
index f9feba174..10cd3dc4c 100644
--- a/restructuring/analysis/facts/edf.v
+++ b/restructuring/analysis/facts/edf.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.model.priority.edf.
-Require Export rt.restructuring.model.task.absolute_deadline.
+Require Import rt.restructuring.model.priority.edf.
+Require Import rt.restructuring.model.task.absolute_deadline.
 
 (** In this section, we prove a few properties about EDF policy. *)
 Section PropertiesOfEDF.
diff --git a/restructuring/analysis/facts/priority_inversion_is_bounded.v b/restructuring/analysis/facts/priority_inversion_is_bounded.v
index 33fa5cd7a..93c89d784 100644
--- a/restructuring/analysis/facts/priority_inversion_is_bounded.v
+++ b/restructuring/analysis/facts/priority_inversion_is_bounded.v
@@ -3,6 +3,9 @@ Require Export rt.restructuring.model.schedule.priority_driven.
 Require Export rt.restructuring.analysis.facts.no_carry_in_exists.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
+
 (** Throughout the file we assume for the classic Liu & Layland model
     of readiness without jitter and no self-suspensions, where
     pending jobs are always ready. *)
diff --git a/restructuring/analysis/facts/readiness/basic.v b/restructuring/analysis/facts/readiness/basic.v
index 5875f8546..c10e406bb 100644
--- a/restructuring/analysis/facts/readiness/basic.v
+++ b/restructuring/analysis/facts/readiness/basic.v
@@ -1,6 +1,8 @@
-Require Export rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.analysis.basic_facts.completion.
 
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+Require Import rt.restructuring.model.readiness.basic.
+
 Section LiuAndLaylandReadiness.
   (** Consider any kind of jobs... *)
   Context {Job : JobType}.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
index 988413f76..18e002d13 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
@@ -7,6 +7,7 @@ Require Import rt.restructuring.model.processor.ideal.
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
 Require Import rt.restructuring.model.readiness.basic.
 
+Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
index 214f39696..099c7bf59 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
@@ -7,6 +7,7 @@ Require Import rt.restructuring.model.processor.ideal.
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
 Require Import rt.restructuring.model.readiness.basic.
 
+Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.limited_preemptive.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/schedulability.v b/restructuring/analysis/schedulability.v
index 9c0bd70fc..a3de0ced0 100644
--- a/restructuring/analysis/schedulability.v
+++ b/restructuring/analysis/schedulability.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.model.task.absolute_deadline.
 Require Export rt.restructuring.analysis.basic_facts.completion.
+Require Import rt.restructuring.model.task.absolute_deadline.
 
 Section Task.
   Context {Task : TaskType}.
diff --git a/restructuring/model/schedule/limited_preemptive.v b/restructuring/model/schedule/limited_preemptive.v
index 2cc39396f..a69d30dc6 100644
--- a/restructuring/model/schedule/limited_preemptive.v
+++ b/restructuring/model/schedule/limited_preemptive.v
@@ -1,8 +1,9 @@
-Require Export rt.restructuring.model.processor.ideal.
-Require Export rt.restructuring.model.preemption.parameter.
- 
+Require Export rt.restructuring.model.preemption.parameter. 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
+
 (** * Schedule with Limited Preemptions *)
 (** In this section we introduce the notion of preemptions-aware
     schedule. *)
diff --git a/restructuring/model/schedule/preemption_time.v b/restructuring/model/schedule/preemption_time.v
index 790fd66f7..df873a285 100644
--- a/restructuring/model/schedule/preemption_time.v
+++ b/restructuring/model/schedule/preemption_time.v
@@ -1,7 +1,9 @@
-Require Export rt.restructuring.model.processor.ideal.
 Require Export rt.restructuring.model.preemption.parameter.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
+
 (** * Preemption Time in Ideal Uni-Processor Model *)
 (** In this section we define the notion of preemption _time_ for
     ideal uni-processor model. *)
diff --git a/restructuring/model/schedule/tdma.v b/restructuring/model/schedule/tdma.v
index 7b32d2dbc..6175d3d00 100644
--- a/restructuring/model/schedule/tdma.v
+++ b/restructuring/model/schedule/tdma.v
@@ -1,9 +1,11 @@
 Require Export rt.restructuring.model.task.concept.
-Require Export rt.restructuring.model.processor.ideal.
 Require Export rt.util.seqset.
 Require Export rt.util.rel.
 From mathcomp Require Export ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div.
 
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
+
 (** In this section, we define the TDMA policy.*)
 Section TDMAPolicy.
 
diff --git a/restructuring/model/task/preemption/limited_preemptive.v b/restructuring/model/task/preemption/limited_preemptive.v
index aa33cabca..5b6b7f687 100644
--- a/restructuring/model/task/preemption/limited_preemptive.v
+++ b/restructuring/model/task/preemption/limited_preemptive.v
@@ -1,8 +1,8 @@
-Require Export rt.restructuring.model.preemption.limited_preemptive.
 Require Export rt.restructuring.model.task.preemption.parameters.
-
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
+Require Import rt.restructuring.model.preemption.limited_preemptive.
+
 (** * Platform for Models with Limited Preemptions *)
 (** In this section, we introduce a set of requirements for function
     [task_preemption_points], so it is coherent with limited
-- 
GitLab