Don't Export modules that introduce new Instances

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

restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v

 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.

restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v

 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.

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.

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.

restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v

 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.

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.

restructuring/analysis/facts/edf.v

-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.

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. *)

restructuring/analysis/facts/readiness/basic.v

-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}.

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.

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.

restructuring/analysis/schedulability.v

-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}.

restructuring/model/schedule/limited_preemptive.v

-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. *)

restructuring/model/schedule/preemption_time.v

-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. *)

restructuring/model/schedule/tdma.v

 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.
 

restructuring/model/task/preemption/limited_preemptive.v

-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