diff --git a/restructuring/analysis/abstract/core/abstract_rta.v b/restructuring/analysis/abstract/core/abstract_rta.v
index cdd9633bbe1b9ff5e65b6e129b25937c65639337..fe5bd0e9e516c0db70d07768abb63a2cb5341245 100644
--- a/restructuring/analysis/abstract/core/abstract_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_rta.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.preemption.task.parameters.
diff --git a/restructuring/analysis/abstract/core/abstract_seq_rta.v b/restructuring/analysis/abstract/core/abstract_seq_rta.v
index a3c9c216761590278ff178ef2d891c570c139415..b28114eb035613c3a00eb7529d876d9807612d49 100644
--- a/restructuring/analysis/abstract/core/abstract_seq_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_seq_rta.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
diff --git a/restructuring/analysis/abstract/core/definitions.v b/restructuring/analysis/abstract/core/definitions.v
index 22f555066f5d743cc6b4eccd93949b9b0ffb0ae9..22116f1dd728685b7215adafc59f1446995d361d 100644
--- a/restructuring/analysis/abstract/core/definitions.v
+++ b/restructuring/analysis/abstract/core/definitions.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
 Require Export rt.restructuring.behavior.all.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.processor.ideal.
   
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/abstract/core/reduction_of_search_space.v b/restructuring/analysis/abstract/core/reduction_of_search_space.v
index d6b403ffdd09c92fc20989aa92c810f2091bafee..ec0e022492c71dfdc2635b3f3246b40ba2ce346c 100644
--- a/restructuring/analysis/abstract/core/reduction_of_search_space.v
+++ b/restructuring/analysis/abstract/core/reduction_of_search_space.v
@@ -1,7 +1,6 @@
 Require Import rt.util.epsilon.
 Require Import rt.util.tactics.
-Require Import rt.restructuring.model.task.
-
+Require Import rt.restructuring.model.task.concept.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** * Reduction of the serach space for Abstract RTA *)
diff --git a/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v b/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
index cb9f38f5db3cc70fa844f400062fa35717abe773..00a4644ac5751900647e2ab984c2222fbe4dda48 100644
--- a/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
+++ b/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Export rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
diff --git a/restructuring/analysis/abstract/instantiations/ideal_processor.v b/restructuring/analysis/abstract/instantiations/ideal_processor.v
index 41901dc53d07a7dbc1aae0647fa87d68052c3efe..6ecd2d6943c38ba29c4758be121ea8fcbf89e571 100644
--- a/restructuring/analysis/abstract/instantiations/ideal_processor.v
+++ b/restructuring/analysis/abstract/instantiations/ideal_processor.v
@@ -1,5 +1,5 @@
 Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.task.
+Require Export rt.restructuring.model.task.concept.
 Require Export rt.restructuring.model.aggregate.workload.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.task.sequential.
diff --git a/restructuring/analysis/arrival/rbf.v b/restructuring/analysis/arrival/rbf.v
index 87f9fcde0b1ef2b727d1b2575b7590f0d5432b8f..bde7b2ae1bb3aa828e6675e7a01f32582ecba6ee 100644
--- a/restructuring/analysis/arrival/rbf.v
+++ b/restructuring/analysis/arrival/rbf.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
 Require Export rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.aggregate.task_arrivals.
 Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
diff --git a/restructuring/analysis/arrival/workload_bound.v b/restructuring/analysis/arrival/workload_bound.v
index bdb5ba43e4018528842cb91852c1a2ce48ed53fb..07be1832e592b0fd8e790a0c905b06e19299f34c 100644
--- a/restructuring/analysis/arrival/workload_bound.v
+++ b/restructuring/analysis/arrival/workload_bound.v
@@ -1,6 +1,6 @@
 Require Import rt.util.sum.
 Require Export rt.restructuring.behavior.all.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.aggregate.task_arrivals.
 Require Import rt.restructuring.model.arrival.arrival_curves.
diff --git a/restructuring/analysis/basic_facts/preemption/job/limited.v b/restructuring/analysis/basic_facts/preemption/job/limited.v
index 18f6c9c7c0f5fc099860e757df43bd0382dfe61c..c10c941336bca54c93b2410cf7c57d37d0e9e28f 100644
--- a/restructuring/analysis/basic_facts/preemption/job/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/job/limited.v
@@ -2,8 +2,7 @@ Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
-
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.valid_schedule.
 Require Import rt.restructuring.model.preemption.job.parameters.
diff --git a/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
index d647b3942d4391a0a8ebbe242db3adbf15f84901..727b6a712ecd18246db200cd653a939ced01f190 100644
--- a/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.schedule.nonpreemptive.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
index b76e25200ff34ac6ed9b1d70ffe282cbae1af5ef..31d9f79259778e27c22e14071a02f9d43adebcc2 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.preemption.task.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
index 8e0d187cd27b18fdf225ef25421a6ab22533ded4..63689bce16f21afae33708aff2cc2b63872a95f8 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
@@ -1,6 +1,6 @@
 Require Import rt.util.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
index c29e09a133af68039fc12e76baec9ac61d88a9e4..f71f40c61aafb19b1b6a2f520762373e04f006fd 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Import rt.restructuring.behavior.job.
 Require Import rt.restructuring.behavior.schedule.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.preemption.valid_schedule.
 Require Import rt.restructuring.model.preemption.job.parameters.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
index 60cdbe495eafe981697cca072d7eb87e7bb8a65f..52153acc98bdfa7e8fab13305edcc69e3362d92b 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.schedule.nonpreemptive.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
index b6577dce3dc5bb032e5fa0c93655972834938dde..d84813271521bad5fc5484a4cb0a8260998ddce3 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.preemption.job.instance.preemptive.
 Require Import rt.restructuring.model.preemption.task.instance.preemptive.
diff --git a/restructuring/analysis/basic_facts/preemption/task/floating.v b/restructuring/analysis/basic_facts/preemption/task/floating.v
index da27b50bd81d2133a620ab38c205096253b1239b..70284babe480d0feb0002142b85b288af5f10a6d 100644
--- a/restructuring/analysis/basic_facts/preemption/task/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/task/floating.v
@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Import rt.util.nondecreasing.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.preemption.task.parameters.
diff --git a/restructuring/analysis/basic_facts/preemption/task/limited.v b/restructuring/analysis/basic_facts/preemption/task/limited.v
index 67fe37f648255c91b31cb1b3304ed4bb42bbb6bc..7aca2dc6190477fd4e08124ef290deb82b84a774 100644
--- a/restructuring/analysis/basic_facts/preemption/task/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/task/limited.v
@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Import rt.util.nondecreasing.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.preemption.task.parameters.
diff --git a/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
index 00a713699f95ab345c6062a9e9019ec8b5f9f185..fa2bda3ca5f27cbf12af5d52ad5ccdac918e7b86 100644
--- a/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/task/nonpreemptive.v
@@ -3,7 +3,7 @@ Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.basic_facts.all.
 
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.schedule.nonpreemptive.
 Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
 Require Import rt.restructuring.model.preemption.task.instance.nonpreemptive.
diff --git a/restructuring/analysis/basic_facts/preemption/task/preemptive.v b/restructuring/analysis/basic_facts/preemption/task/preemptive.v
index 3b19eef2c8e827964579176818f87688f6368870..771a37d3f41937a7cd9dee6770e47371db0db6b6 100644
--- a/restructuring/analysis/basic_facts/preemption/task/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/task/preemptive.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.instance.preemptive.
 Require Import rt.restructuring.model.preemption.task.instance.preemptive.
diff --git a/restructuring/analysis/basic_facts/service_of_jobs.v b/restructuring/analysis/basic_facts/service_of_jobs.v
index 93741e6f15b62f50c0d5d84caf831a94dd626aca..698a63177683e4aacb7361980f3e6fce26a307ea 100644
--- a/restructuring/analysis/basic_facts/service_of_jobs.v
+++ b/restructuring/analysis/basic_facts/service_of_jobs.v
@@ -1,7 +1,7 @@
 Require Import rt.util.all.
 
 Require Import rt.restructuring.behavior.all.
-Require Export rt.restructuring.model.task.
+Require Export rt.restructuring.model.task.concept.
 Require Export rt.restructuring.model.aggregate.workload.
 Require Export rt.restructuring.model.aggregate.service_of_jobs.
 Require Export rt.restructuring.model.processor.ideal.
diff --git a/restructuring/analysis/definitions/busy_interval.v b/restructuring/analysis/definitions/busy_interval.v
index d0ab1ec1a3902fa3620cc1f178ae22aef7b31475..0857ebc79f1d523b1fff9f404b442651063d50bf 100644
--- a/restructuring/analysis/definitions/busy_interval.v
+++ b/restructuring/analysis/definitions/busy_interval.v
@@ -2,7 +2,7 @@ Require Export rt.util.all.
 Require Export rt.restructuring.behavior.all.
 Require Export rt.restructuring.analysis.basic_facts.all.
 Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.task.
+Require Export rt.restructuring.model.task.concept.
 Require Export rt.restructuring.model.schedule.work_conserving.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/definitions/no_carry_in.v b/restructuring/analysis/definitions/no_carry_in.v
index f9131ff557aa87a33f84c9e2fe9d15700d2d58bb..2118f1c9ff870365e5d462965a8f97a72d3aab89 100644
--- a/restructuring/analysis/definitions/no_carry_in.v
+++ b/restructuring/analysis/definitions/no_carry_in.v
@@ -2,8 +2,7 @@ Require Export rt.util.all.
 Require Export rt.restructuring.behavior.all.
 Require Export rt.restructuring.analysis.basic_facts.all.
 Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.task.
-
+Require Export rt.restructuring.model.task.concept.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (** * No Carry-In *)
diff --git a/restructuring/analysis/definitions/priority_inversion.v b/restructuring/analysis/definitions/priority_inversion.v
index ff1eca46d53b89852c25ba1b7d4cc9dc9eee06f8..559b0a207be062afa14971f9fb69842c2209ea9b 100644
--- a/restructuring/analysis/definitions/priority_inversion.v
+++ b/restructuring/analysis/definitions/priority_inversion.v
@@ -2,7 +2,7 @@ Require Export rt.util.all.
 Require Export rt.restructuring.behavior.all.
 Require Export rt.restructuring.analysis.basic_facts.all.
 Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.task.
+Require Export rt.restructuring.model.task.concept.
 Require Export rt.restructuring.model.schedule.work_conserving.
 Require Export rt.restructuring.model.priority.classes.
 Require Export rt.restructuring.analysis.definitions.busy_interval.
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 6eed5c6bcb2800f7e2aa7e4ad7eff9c3e522fd26..71e1e4c665d19f55f4a72f2c6d573bcf7cb23d11 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.aggregate.workload.
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
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 6b77d1bbab49be336bc97f969f5cef76473d8a63..b8e4da568d2fc3b6a8ebeee070a7ab63d0a414e1 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.aggregate.workload.
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
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 2b964a28a0b1233e5fc8094bc61bf1fa4b56afe0..65b36f528c46da306090b85ee2b9693914930c61 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.aggregate.workload.
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
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 9f864f23e84ba8229dca36eaf07496b9145d2bb2..edd6f9162fe1d77cbfe37ba73094f304bda2d8b8 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.aggregate.workload.
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
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 65b7a144ee5a406472d7af6330bb4229168667d8..ccb737e69438aa4563f52823f40deec1db43b243 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.aggregate.workload.
 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 41edf3e0b179aa3830558d7a7df85f7696214ee7..931ed0aa6b6d09b2545f03003972fbc320661137 100644
--- a/restructuring/analysis/edf/rta/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/response_time_bound.v
@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.aggregate.workload.
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
diff --git a/restructuring/analysis/facts/busy_interval_exists.v b/restructuring/analysis/facts/busy_interval_exists.v
index 14748080bbdb9bfc5a51f69dc8abe79ae0ae8985..d5600eb1dfc8d29f2d698f26ecd0c39ebd57089e 100644
--- a/restructuring/analysis/facts/busy_interval_exists.v
+++ b/restructuring/analysis/facts/busy_interval_exists.v
@@ -2,7 +2,7 @@ Require Export rt.util.all.
 Require Export rt.restructuring.behavior.all.
 Require Export rt.restructuring.analysis.basic_facts.all.
 Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.task.
+Require Export rt.restructuring.model.task.concept.
 Require Export rt.restructuring.model.schedule.work_conserving.
 Require Export rt.restructuring.model.priority.classes.
 Require Export rt.restructuring.analysis.definitions.busy_interval.
diff --git a/restructuring/analysis/facts/no_carry_in_exists.v b/restructuring/analysis/facts/no_carry_in_exists.v
index 78ca3122eb7fd96a448c0903a5820be700016613..196b6376c1b10e6436a30da88ae5fe3a3525e83c 100644
--- a/restructuring/analysis/facts/no_carry_in_exists.v
+++ b/restructuring/analysis/facts/no_carry_in_exists.v
@@ -2,7 +2,7 @@ Require Export rt.util.all.
 Require Export rt.restructuring.behavior.all.
 Require Export rt.restructuring.analysis.basic_facts.all.
 Require Export rt.restructuring.analysis.definitions.job_properties.
-Require Export rt.restructuring.model.task.
+Require Export rt.restructuring.model.task.concept.
 Require Export rt.restructuring.model.schedule.work_conserving.
 Require Export rt.restructuring.model.priority.classes.
 Require Export rt.restructuring.analysis.definitions.no_carry_in.
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 aa8cf8ee9353eed018ecab2148bcb7dd5263e92c..e48ce1209992ec2d030dface138e430db13d66a9 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
@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.aggregate.workload.
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
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 a7b5a7526d71b2f23ac457b15d5dae386b6e3b95..f93f2e8f2bb3806a96bc65290cf0cd4bd436f3bc 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
@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.aggregate.workload.
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
index 6491faac461784858c08bdad8e01fec99d6da60a..e2387d28ef594e4d5422ff95a2741f13cbdb3c19 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.aggregate.workload.
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
index 792b7badd7c383c5ca0c86a6b217fb332054625c..9b0e59e26e7b135752994edf0e0d2a246bd25eb5 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.aggregate.workload.
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
index c77c2eddf5a5467366b20b3e800cd1a18bc5e8ef..85d7f787894ad56c9bdbfd5d7feacbd8cee72c21 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.aggregate.workload.
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
diff --git a/restructuring/analysis/fixed_priority/rta/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
index dad6bcae4398876f57a012abdbbbc4329d6d6e89..18e460ccd13cf99b483c8f59006ef077857bf362 100644
--- a/restructuring/analysis/fixed_priority/rta/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.
+Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.aggregate.workload.
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
diff --git a/restructuring/analysis/task_schedule.v b/restructuring/analysis/task_schedule.v
index ec3fd834fc346f05d99256d43a1fa959d48dcd15..2f7eb103e49e347c085393f1a0c54177b7c6f4ba 100644
--- a/restructuring/analysis/task_schedule.v
+++ b/restructuring/analysis/task_schedule.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.task.
+Require Export rt.restructuring.model.task.concept.
 Require Export rt.restructuring.analysis.basic_facts.ideal_schedule.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/model/aggregate/task_arrivals.v b/restructuring/model/aggregate/task_arrivals.v
index 585ff897e2cffa0cc68c6815533939736b23141d..9216784b1bc934f0750ac8c67685d9250ae055ec 100644
--- a/restructuring/model/aggregate/task_arrivals.v
+++ b/restructuring/model/aggregate/task_arrivals.v
@@ -1,5 +1,4 @@
-Require Export rt.restructuring.model.task.
-
+Require Export rt.restructuring.model.task.concept.
 (** In this file we provide basic definitions related to tasks on arrival sequences. *)
 Section TaskArrivals.
 
diff --git a/restructuring/model/arrival/sporadic.v b/restructuring/model/arrival/sporadic.v
index 3806e931c63aecc1a14336cae96534ddef1a286a..23b36230c1e71d67464588140d76d26de5efcf8a 100644
--- a/restructuring/model/arrival/sporadic.v
+++ b/restructuring/model/arrival/sporadic.v
@@ -1,5 +1,4 @@
-Require Export rt.restructuring.model.task.
-
+Require Export rt.restructuring.model.task.concept.
 Section TaskMinInterArrivalTime.
   Context {Task : TaskType}.
 
diff --git a/restructuring/model/preemption/task/parameters.v b/restructuring/model/preemption/task/parameters.v
index cb701952f1bbfa06aa09e5acbaeef7f3503d7e24..d4307eacdd03ece89c4aeb692e26b1271b4c72e7 100644
--- a/restructuring/model/preemption/task/parameters.v
+++ b/restructuring/model/preemption/task/parameters.v
@@ -1,6 +1,5 @@
 Require Export rt.util.all.
-Require Export rt.restructuring.model.task.
-
+Require Export rt.restructuring.model.task.concept.
 (** * Static information about preemption points *)
 
 (** Definition of a generic type of parameter relating a task 
diff --git a/restructuring/model/priority/classes.v b/restructuring/model/priority/classes.v
index cf4bd4b21ea91d2d1a98bd0190a193485aac5927..138496cee2fcf2623b68c79ff9ddb9b09dee31e4 100644
--- a/restructuring/model/priority/classes.v
+++ b/restructuring/model/priority/classes.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.task.
+Require Export rt.restructuring.model.task.concept.
 Require Export rt.util.rel.
 Require Export rt.util.list.
 
diff --git a/restructuring/model/schedule/tdma.v b/restructuring/model/schedule/tdma.v
index 12510dfaa526c10f77bae394fb0357d24fb5df39..7b32d2dbc94871cab7f10a35c0dc89944cbe0f1c 100644
--- a/restructuring/model/schedule/tdma.v
+++ b/restructuring/model/schedule/tdma.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.task.
+Require Export rt.restructuring.model.task.concept.
 Require Export rt.restructuring.model.processor.ideal.
 Require Export rt.util.seqset.
 Require Export rt.util.rel.
diff --git a/restructuring/model/task/absolute_deadline.v b/restructuring/model/task/absolute_deadline.v
index 7ead8087b183fcf00d5ae63b0a8ca2107d97631f..b32ac00e84d7fa55b4e34139954bd650dffce473 100644
--- a/restructuring/model/task/absolute_deadline.v
+++ b/restructuring/model/task/absolute_deadline.v
@@ -1,5 +1,4 @@
-Require Export rt.restructuring.model.task.
-
+Require Export rt.restructuring.model.task.concept.
 (** Given task deadlines and a mapping from jobs to tasks 
    we provide a generic definition of job_deadline. *)
 Instance job_deadline_from_task_deadline (Job : JobType) (Task : TaskType)
diff --git a/restructuring/model/task.v b/restructuring/model/task/concept.v
similarity index 100%
rename from restructuring/model/task.v
rename to restructuring/model/task/concept.v
diff --git a/restructuring/model/task/sequential.v b/restructuring/model/task/sequential.v
index 4c108a9b5a1f789be55e6d71db610909ce41caac..c52d2c940e70eaec45a60a3efa45989ccca8ac6a 100644
--- a/restructuring/model/task/sequential.v
+++ b/restructuring/model/task/sequential.v
@@ -1,5 +1,4 @@
-Require Export rt.restructuring.model.task.
-
+Require Export rt.restructuring.model.task.concept.
 Section PropertyOfSequentiality.
 
   (** Consider any type of job associated with any type of tasks... *)