diff --git a/restructuring/model/aggregate/service_of_jobs.v b/restructuring/model/aggregate/service_of_jobs.v
index b8ade10471fe442d3f7b205abc42fac2f59cb791..dea1e4ea938f4863b23fdceece8c4add6ce19929 100644
--- a/restructuring/model/aggregate/service_of_jobs.v
+++ b/restructuring/model/aggregate/service_of_jobs.v
@@ -10,100 +10,100 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 (** In this file, we define the notion of service received by a set of jobs. *)
 Section ServiceOfJobs.
 
-  (* Consider any type of tasks ... *)
+  (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
   
-  (*  ... and any type of jobs associated with these tasks. *)
+  (**  ... and any type of jobs associated with these tasks. *)
   Context {Job : JobType}.
   Context `{JobTask Job Task}.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
   
-  (* Consider any kind of processor state model, ... *)
+  (** Consider any kind of processor state model, ... *)
   Context {PState : Type}.
   Context `{ProcessorState Job PState}.
 
-  (* ... any job arrival sequence, ... *) 
+  (** ... any job arrival sequence, ... *) 
   Variable arr_seq : arrival_sequence Job.
 
-  (* ... and any given schedule. *)
+  (** ... and any given schedule. *)
   Variable sched : schedule PState.
   
-  (* First, we define the service received by a generic set of jobs. *)
+  (** First, we define the service received by a generic set of jobs. *)
   Section ServiceOfSetOfJobs.
 
-    (* Let P be any predicate over jobs, ...*)
+    (** Let P be any predicate over jobs, ...*)
     Variable P : Job -> bool.
     
-    (* ... and let jobs denote any (finite) set of jobs. *)
+    (** ... and let jobs denote any (finite) set of jobs. *)
     Variable jobs : seq Job.
 
-    (* Then we define the cumulative service received at 
+    (** Then we define the cumulative service received at 
        time t by the jobs that satisfy this predicate ... *)
     Definition service_of_jobs_at (t : instant) :=
       \sum_(j <- jobs | P j) service_at sched j t.
     
-    (* ... and the cumulative service received during time 
+    (** ... and the cumulative service received during time 
        interval [t1, t2) by the jobs that satisfy the predicate. *)
     Definition service_of_jobs (t1 t2 : instant) :=
       \sum_(j <- jobs | P j) service_during sched j t1 t2.
 
   End ServiceOfSetOfJobs.
   
-  (* Next, we define the service received by tasks with 
+  (** Next, we define the service received by tasks with 
      higher-or-equal priority under a given FP policy. *)
   Section PerTaskPriority.
 
-    (* Consider any FP policy. *)
+    (** Consider any FP policy. *)
     Variable higher_eq_priority : FP_policy Task.
     
-    (* Let jobs denote any (finite) set of jobs. *)
+    (** Let jobs denote any (finite) set of jobs. *)
     Variable jobs : seq Job.
 
-    (* Let tsk be the task to be analyzed. *)
+    (** Let tsk be the task to be analyzed. *)
     Variable tsk : Task.
 
-    (* Based on the definition of jobs of higher or equal priority (with respect to tsk), ... *)
+    (** Based on the definition of jobs of higher or equal priority (with respect to tsk), ... *)
     Let of_higher_or_equal_priority j := higher_eq_priority (job_task j) tsk.
     
-    (* ...we define the service received during [t1, t2) by jobs of higher or equal priority. *)
+    (** ...we define the service received during [t1, t2) by jobs of higher or equal priority. *)
     Definition service_of_higher_or_equal_priority_tasks (t1 t2 : instant) :=
       service_of_jobs of_higher_or_equal_priority jobs t1 t2.
 
   End PerTaskPriority.
   
-  (* Next, we define the service received by jobs with 
+  (** Next, we define the service received by jobs with 
      higher-or-equal  priority under JLFP policies. *)
   Section PerJobPriority.
 
-    (* Consider any JLDP policy. *)
+    (** Consider any JLDP policy. *)
     Variable higher_eq_priority : JLFP_policy Job.
     
-    (* Let jobs denote any (finite) set of jobs. *)
+    (** Let jobs denote any (finite) set of jobs. *)
     Variable jobs : seq Job.
 
-    (* Let j be the job to be analyzed. *)
+    (** Let j be the job to be analyzed. *)
     Variable j : Job.
 
-    (* Based on the definition of jobs of higher or equal priority, ... *)
+    (** Based on the definition of jobs of higher or equal priority, ... *)
     Let of_higher_or_equal_priority j_hp := higher_eq_priority j_hp j.
     
-    (* ...we define the service received during [t1, t2) by jobs of higher or equal priority. *)
+    (** ...we define the service received during [t1, t2) by jobs of higher or equal priority. *)
     Definition service_of_higher_or_equal_priority_jobs (t1 t2 : instant) :=
       service_of_jobs of_higher_or_equal_priority jobs t1 t2.
 
   End PerJobPriority.
 
-  (* In this section, we define the notion of workload for sets of jobs. *)  
+  (** In this section, we define the notion of workload for sets of jobs. *)  
   Section ServiceOfTask.
     
-    (* Let tsk be the task to be analyzed... *)
+    (** Let tsk be the task to be analyzed... *)
     Variable tsk : Task. 
 
-    (* ... and let jobs denote any (finite) set of jobs. *)
+    (** ... and let jobs denote any (finite) set of jobs. *)
     Variable jobs : seq Job.
 
-    (* We define the cumulative task service received by 
+    (** We define the cumulative task service received by 
        the jobs from the task within time interval [t1, t2). *)
     Definition task_service_of_jobs_in t1 t2 :=
       service_of_jobs (job_of_task tsk) jobs t1 t2.
diff --git a/restructuring/model/aggregate/task_arrivals.v b/restructuring/model/aggregate/task_arrivals.v
index 428f2ede03e36a9f7668f1d01113cb9074c2e240..914ec2178a34c30a18ad12dda0fb3791e4fb7299 100644
--- a/restructuring/model/aggregate/task_arrivals.v
+++ b/restructuring/model/aggregate/task_arrivals.v
@@ -1,43 +1,43 @@
 From rt.restructuring.model Require Export task.
 
-(* In this file we provide basic definitions related to tasks on arrival sequences. *)
+(** In this file we provide basic definitions related to tasks on arrival sequences. *)
 Section TaskArrivals.
 
-  (* Consider any type of job associated with any type of tasks. *)
+  (** Consider any type of job associated with any type of tasks. *)
   Context {Job : JobType}.
   Context {Task : TaskType}.
   Context `{JobTask Job Task}.
 
-  (* Consider any job arrival sequence. *)
+  (** Consider any job arrival sequence. *)
   Variable arr_seq : arrival_sequence Job.
 
   Section Definitions.
 
-    (* Let tsk be any task. *)
+    (** Let tsk be any task. *)
     Variable tsk : Task.
 
-    (* We define the sequence of jobs of tsk arriving at time t. *)
+    (** We define the sequence of jobs of tsk arriving at time t. *)
     Definition task_arrivals_at (t : instant) : seq Job :=
       [seq j <- arrivals_at arr_seq t | job_task j == tsk].
 
-    (* By concatenation, we construct the list of jobs of tsk that arrived in the
+    (** By concatenation, we construct the list of jobs of tsk that arrived in the
        interval [t1, t2). *)
     Definition task_arrivals_between (t1 t2 : instant) :=
       [seq j <- arrivals_between arr_seq t1 t2 | job_task j == tsk].
 
-    (* Based on that, we define the list of jobs of tsk that arrived up to time t, ...*)
+    (** Based on that, we define the list of jobs of tsk that arrived up to time t, ...*)
     Definition task_arrivals_up_to (t : instant) := task_arrivals_between 0 t.+1.
 
-    (* ...and the list of jobs of tsk that arrived strictly before time t ... *)
+    (** ...and the list of jobs of tsk that arrived strictly before time t ... *)
     Definition task_arrivals_before (t : instant) := task_arrivals_between 0 t.
 
-    (* ... and also count the number of job arrivals. *)
+    (** ... and also count the number of job arrivals. *)
     Definition number_of_task_arrivals (t1 t2 : instant) :=
       size (task_arrivals_between t1 t2).
     
   End Definitions.
 
-  (* We define a predicate for arrival sequences for which jobs come from a taskset. *)
+  (** We define a predicate for arrival sequences for which jobs come from a taskset. *)
   Definition arrivals_come_from_taskset (ts : seq Task) :=
     forall j, arrives_in arr_seq j -> job_task j \in ts.
 
diff --git a/restructuring/model/aggregate/workload.v b/restructuring/model/aggregate/workload.v
index 0160115f3e066a81c86e48e43bf7ba7bb4a48d0c..e0485715f8860f5a7f8cc05c2da18473a36ac0db 100644
--- a/restructuring/model/aggregate/workload.v
+++ b/restructuring/model/aggregate/workload.v
@@ -8,86 +8,86 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 (** In this section, we define the notion of workload for sets of jobs. *)  
 Section WorkloadOfJobs.
 
-  (* Consider any type of tasks ... *)
+  (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
   Context `{TaskCost Task}.
 
-  (*  ... and any type of jobs associated with these tasks. *)
+  (**  ... and any type of jobs associated with these tasks. *)
   Context {Job : JobType}.
   Context `{JobTask Job Task}.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
 
-  (* Consider any job arrival sequence. *)
+  (** Consider any job arrival sequence. *)
   Variable arr_seq : arrival_sequence Job.
   
-  (* First, we define the workload for generic sets of jobs. *)
+  (** First, we define the workload for generic sets of jobs. *)
   Section WorkloadOfJobs.
     
-    (* Given any predicate over Jobs, ... *)
+    (** Given any predicate over Jobs, ... *)
     Variable P : Job -> bool.
 
-    (* ... and any (finite) set of jobs. *)
+    (** ... and any (finite) set of jobs. *)
     Variable jobs : seq Job.
 
-    (* We define the total workload of the jobs that satisfy predicate P. *)
+    (** We define the total workload of the jobs that satisfy predicate P. *)
     Definition workload_of_jobs := \sum_(j <- jobs | P j) job_cost j.
     
   End WorkloadOfJobs.
 
-  (* Next, we define the workload of tasks with higher or 
+  (** Next, we define the workload of tasks with higher or 
      equal priority under FP policies. *)
   Section PerTaskPriority.
 
-    (* Consider any FP policy that indicates whether a task has
+    (** Consider any FP policy that indicates whether a task has
        higher or equal priority. *)
     Variable higher_eq_priority : FP_policy Task.
 
-    (* Let tsk be the task to be analyzed. *)
+    (** Let tsk be the task to be analyzed. *)
     Variable tsk : Task.
 
-    (* Recall the notion of a job of higher or equal priority. *)
+    (** Recall the notion of a job of higher or equal priority. *)
     Let of_higher_or_equal_priority j :=
       higher_eq_priority (job_task j) tsk.
     
-    (* Then, we define the workload of all jobs of tasks with
+    (** Then, we define the workload of all jobs of tasks with
        higher-or-equal priority than tsk. *)
     Definition workload_of_higher_or_equal_priority_tasks :=
       workload_of_jobs of_higher_or_equal_priority.
 
   End PerTaskPriority.
 
-  (* Then, we define the workload of jobs with higher or
+  (** Then, we define the workload of jobs with higher or
      equal priority under JLFP policies. *)
   Section PerJobPriority.
 
-    (* Consider any JLFP policy that indicates whether a job has
+    (** Consider any JLFP policy that indicates whether a job has
        higher or equal priority. *)
     Variable higher_eq_priority : JLFP_policy Job.
 
-    (* Let j be the job to be analyzed. *)
+    (** Let j be the job to be analyzed. *)
     Variable j : Job.
 
-    (* Recall the notion of a job of higher or equal priority. *)
+    (** Recall the notion of a job of higher or equal priority. *)
     Let of_higher_or_equal_priority j_hp := higher_eq_priority j_hp j.
     
-    (* Then, we define the workload of higher or equal priority of all jobs
+    (** Then, we define the workload of higher or equal priority of all jobs
        with higher-or-equal priority than j. *)
     Definition workload_of_higher_or_equal_priority_jobs :=
       workload_of_jobs of_higher_or_equal_priority.
 
   End PerJobPriority.
 
-  (* We also define workload of a task. *)
+  (** We also define workload of a task. *)
   Section TaskWorkload.
     
-    (* Let tsk be the task to be analyzed. *)
+    (** Let tsk be the task to be analyzed. *)
     Variable tsk : Task.
     
-    (* We define the task workload as the workload of jobs of task tsk. *)
+    (** We define the task workload as the workload of jobs of task tsk. *)
     Definition task_workload jobs := workload_of_jobs (job_of_task tsk) jobs.
 
-    (* Next, we recall the definition of the task workload in interval [t1, t2). *)
+    (** Next, we recall the definition of the task workload in interval [t1, t2). *)
     Definition task_workload_between (t1 t2 : instant) :=
       task_workload (arrivals_between arr_seq t1 t2).
     
diff --git a/restructuring/model/arrival/arrival_curves.v b/restructuring/model/arrival/arrival_curves.v
index 4a7c2bf6273925ed455f4ebc6fe4475e15cce448..75ea17cc7bbf949dcafe7ed79ce834cb06044f49 100644
--- a/restructuring/model/arrival/arrival_curves.v
+++ b/restructuring/model/arrival/arrival_curves.v
@@ -2,38 +2,38 @@ From rt.util Require Import all.
 From rt.restructuring.behavior Require Export all.
 From rt.restructuring.model Require Import task_arrivals.
 
-(* In this section, we define the notion of arrival curves, which
+(** In this section, we define the notion of arrival curves, which
    can be used to reason about the frequency of job arrivals. *)
 Section ArrivalCurves.
 
-  (* Consider any type of tasks ... *)
+  (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
 
-  (*  ... and any type of jobs associated with these tasks. *)
+  (**  ... and any type of jobs associated with these tasks. *)
   Context {Job : JobType}.
   Context `{JobTask Job Task}.
 
- (* Consider any job arrival sequence. *)
+ (** Consider any job arrival sequence. *)
   Variable arr_seq : arrival_sequence Job.
 
-  (* First, we define what constitutes an arrival bound for a task. *)
+  (** First, we define what constitutes an arrival bound for a task. *)
   Section ArrivalCurves.
 
-    (* We say that num_arrivals is a valid arrival curve for task tsk iff
+    (** We say that num_arrivals is a valid arrival curve for task tsk iff
        [num_arrivals] is a monotonic function that equals 0 for the empty 
        interval delta = 0. *)
     Definition valid_arrival_curve (tsk : Task) (num_arrivals : duration -> nat) :=
       num_arrivals 0 = 0 /\
       monotone num_arrivals leq.
 
-    (* We say that max_arrivals is an upper arrival bound for tsk iff, for any interval [t1, t2),
+    (** We say that max_arrivals is an upper arrival bound for tsk iff, for any interval [t1, t2),
        [max_arrivals (t2 - t1)] bounds the number of jobs of tsk that arrive in that interval. *)
     Definition respects_max_arrivals (tsk : Task) (max_arrivals : duration -> nat) :=
       forall (t1 t2 : instant),
         t1 <= t2 ->
         number_of_task_arrivals arr_seq tsk t1 t2 <= max_arrivals (t2 - t1).
 
-    (* We define in the same way lower arrival bounds. *)
+    (** We define in the same way lower arrival bounds. *)
     Definition respects_min_arrivals (tsk : Task) (min_arrivals : duration -> nat) :=
       forall (t1 t2 : instant),
         t1 <= t2 ->
@@ -43,7 +43,7 @@ Section ArrivalCurves.
 
   Section SeparationBound.
 
-    (* Then, we say that min_separation is a lower separation bound iff, for any number of jobs
+    (** Then, we say that min_separation is a lower separation bound iff, for any number of jobs
        of tsk, min_separation lower-bounds the minimum interval length in which that number
        of jobs can be spawned. *)
     Definition respects_min_separation (tsk : Task) (min_separation: nat -> duration) :=
@@ -51,7 +51,7 @@ Section ArrivalCurves.
           t1 <= t2 ->
           min_separation (number_of_task_arrivals arr_seq tsk t1 t2) <= t2 - t1.
 
-    (* We define in the same way upper separation bounds *)
+    (** We define in the same way upper separation bounds *)
     Definition respects_max_separation (tsk : Task) (max_separation: nat -> duration):=
       forall t1 t2,
         t1 <= t2 ->
@@ -61,7 +61,7 @@ Section ArrivalCurves.
 
 End ArrivalCurves.
 
-(* We define generic classes for arrival curves  *)
+(** We define generic classes for arrival curves  *)
 Class MaxArrivals (Task : TaskType) := max_arrivals : Task -> duration -> nat.
 
 Class MinArrivals (Task : TaskType) := min_arrivals : Task -> duration -> nat.
@@ -72,32 +72,32 @@ Class MinSeparation (Task : TaskType) := min_separation : Task -> nat -> duratio
 
 Section ArrivalCurvesModel.
 
-  (* Consider any type of tasks ... *)
+  (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
 
-  (*  ... and any type of jobs associated with these tasks. *)
+  (**  ... and any type of jobs associated with these tasks. *)
   Context {Job : JobType}.
   Context `{JobTask Job Task}.
 
-  (* Consider any job arrival sequence... *)
+  (** Consider any job arrival sequence... *)
   Variable arr_seq : arrival_sequence Job.
 
-  (* ..and all the classes of arrival curves. *) 
+  (** ..and all the classes of arrival curves. *) 
   Context `{MaxArrivals Task}
           `{MinArrivals Task}
           `{MaxSeparation Task}
           `{MinSeparation Task}.
 
-  (* Let ts be an arbitrary task set. *)
+  (** Let ts be an arbitrary task set. *)
   Variable ts : seq Task.
 
-  (* We say that arrivals is a valid arrival curve for a taskset if it is valid for any task
+  (** We say that arrivals is a valid arrival curve for a taskset if it is valid for any task
      in the taskset *)
   Definition valid_taskset_arrival_curve (arrivals : Task -> duration -> nat) :=
     forall (tsk : Task), tsk \in ts -> valid_arrival_curve tsk (arrivals tsk).
 
-  (* We say that max_arrivals is an arrival bound for taskset ts *)
-  (* iff max_arrival is an arrival bound for any task from ts. *)
+  (** We say that max_arrivals is an arrival bound for taskset ts *)
+  (** iff max_arrival is an arrival bound for any task from ts. *)
   Definition taskset_respects_max_arrivals :=
     forall (tsk : Task), tsk \in ts -> respects_max_arrivals arr_seq tsk (max_arrivals tsk).
 
diff --git a/restructuring/model/arrival/sporadic.v b/restructuring/model/arrival/sporadic.v
index fb19b8d1eb6618d7de27ac393acd96c05c84a089..436880829e5432bc34af23d3532460cb00b2c017 100644
--- a/restructuring/model/arrival/sporadic.v
+++ b/restructuring/model/arrival/sporadic.v
@@ -15,18 +15,18 @@ Section TaskMinInterArrivalTime.
 
   Definition respects_sporadic_task_model (tsk : Task) (d : duration) :=
     forall (j j': Job),
-      j <> j' -> (* Given two different jobs j and j' ... *)
-      arrives_in arr_seq j -> (* ...that belong to the arrival sequence... *)
+      j <> j' -> (** Given two different jobs j and j' ... *)
+      arrives_in arr_seq j -> (** ...that belong to the arrival sequence... *)
       arrives_in arr_seq j' ->
       job_task j = tsk ->
-      job_task j' = tsk -> (* ... and that are spawned by the same task, ... *)
-      job_arrival j <= job_arrival j' -> (* ... if the arrival of j precedes the arrival of j' ...,  *)
-      (* then the arrival of j and the arrival of j' are separated by at least one period. *)
+      job_task j' = tsk -> (** ... and that are spawned by the same task, ... *)
+      job_arrival j <= job_arrival j' -> (** ... if the arrival of j precedes the arrival of j' ...,  *)
+      (** then the arrival of j and the arrival of j' are separated by at least one period. *)
       job_arrival j' >= job_arrival j + d.
 
 End TaskMinInterArrivalTime.
 
-(* Definition of a generic type of parameter for task
+(** Definition of a generic type of parameter for task
    minimum inter arrival times *)
 
 Class SporadicModel (Task : TaskType) :=
@@ -46,7 +46,7 @@ Section SporadicModel.
 
   Variable arr_seq : arrival_sequence Job.
 
-  (* Then, we define the sporadic task model as follows.*)
+  (** Then, we define the sporadic task model as follows.*)
   Definition taskset_respects_sporadic_task_model :=
     forall tsk,
       tsk \in ts ->
diff --git a/restructuring/model/job.v b/restructuring/model/job.v
index 9701ef4854009289da46ca164a3d8519516a077a..c0f6c912da5b70f17cf1953d820700af8a302f9f 100644
--- a/restructuring/model/job.v
+++ b/restructuring/model/job.v
@@ -1,17 +1,17 @@
 From rt.restructuring.behavior Require Export all.
 From mathcomp Require Export eqtype ssrnat.
 
-(* In this section, we introduce properties of a job. *)
+(** In this section, we introduce properties of a job. *)
 Section PropertiesOfJob.
 
-  (* Assume that job costs are known. *)
+  (** Assume that job costs are known. *)
   Context {Job : JobType}.
   Context `{JobCost Job}.
 
-  (* Consider an arbitrary job. *)
+  (** Consider an arbitrary job. *)
   Variable j : Job.
 
-  (* The job cost must be positive. *)
+  (** The job cost must be positive. *)
   Definition job_cost_positive := job_cost j > 0.
 
 End PropertiesOfJob. 
\ No newline at end of file
diff --git a/restructuring/model/preemption/preemption_model.v b/restructuring/model/preemption/preemption_model.v
index 0669e2cfa148baac902b87ac934f6fe319a57749..b46b17584cadb772ac1e65e48ab824cb9574d4c8 100644
--- a/restructuring/model/preemption/preemption_model.v
+++ b/restructuring/model/preemption/preemption_model.v
@@ -8,65 +8,65 @@ From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype
     the scheduler will enforce correct behavior. For that, we must 
     define additional predicates. *)
 
-(* Definition of a generic type of parameter relating jobs to their preemption points. *)
+(** Definition of a generic type of parameter relating jobs to their preemption points. *)
 Class JobPreemptable (Job : JobType) := job_preemptable : Job -> duration -> bool.
 
 Section ValidPreemptionModel.
 
-  (* Consider any type of tasks ... *)
+  (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
   Context `{TaskCost Task}.
 
-  (*  ... and any type of jobs associated with these tasks. *)
+  (**  ... and any type of jobs associated with these tasks. *)
   Context {Job : JobType}.
   Context `{JobTask Job Task}.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
 
-  (* In addition, we assume the existence of a function
+  (** In addition, we assume the existence of a function
      maping jobs to theirs preemption points ... *)
   Context `{JobPreemptable Job}.
 
-  (* Consider any kind of processor state model, ... *)
+  (** Consider any kind of processor state model, ... *)
   Context {PState : Type}.
   Context `{ProcessorState Job PState}.
 
-  (* ... any job arrival sequence, ... *)
+  (** ... any job arrival sequence, ... *)
   Variable arr_seq: arrival_sequence Job.
 
-  (* ... and any given schedule. *)
+  (** ... and any given schedule. *)
   Variable sched: schedule PState.
 
-  (* For simplicity, let's define some local names. *)
+  (** For simplicity, let's define some local names. *)
   Let job_pending := pending sched.
   Let job_completed_by := completed_by sched.
   Let job_scheduled_at := scheduled_at sched.
 
-  (* We require that a job has to be executed at least one time instant
+  (** We require that a job has to be executed at least one time instant
      in order to reach a nonpreemptive segment. In other words, a job 
      must start execution to become non-preemptive. *)
   Definition job_cannot_become_nonpreemptive_before_execution (j : Job) :=
     job_preemptable j 0.
     
-  (* And vice versa, a job cannot remain non-preemptive after its completion. *)
+  (** And vice versa, a job cannot remain non-preemptive after its completion. *)
   Definition job_cannot_be_nonpreemptive_after_completion (j : Job) := 
     job_preemptable j (job_cost j).
   
-  (* Next, if a job j is not preemptive at some time instant t, 
+  (** Next, if a job j is not preemptive at some time instant t, 
      then j must be scheduled at time t. *)
   Definition not_preemptive_implies_scheduled (j : Job) :=
     forall t,
       ~~ job_preemptable j (service sched j t) ->
       job_scheduled_at j t. 
 
-  (* A job can start its execution only from a preemption point. *)
+  (** A job can start its execution only from a preemption point. *)
   Definition execution_starts_with_preemption_point (j : Job) := 
     forall prt,
       ~~ job_scheduled_at j prt ->
       job_scheduled_at j prt.+1 ->
       job_preemptable j (service sched j prt.+1).
 
-  (* We say that a preemption model is a valid preemption model if 
+  (** We say that a preemption model is a valid preemption model if 
      all the assumptions given above are satisfied for any job. *)
   Definition valid_preemption_model :=
     forall j,
diff --git a/restructuring/model/processor/platform_properties.v b/restructuring/model/processor/platform_properties.v
index 1ad0b7cb0fa01046f8ba42ca894270ae37120b5d..9beb1443c676f4b19f678157c0088919d7e2f167 100644
--- a/restructuring/model/processor/platform_properties.v
+++ b/restructuring/model/processor/platform_properties.v
@@ -1,24 +1,24 @@
 From rt.restructuring.behavior Require Export all.
 
-(* To reason about classes of schedule types / processor models, we define the
+(** To reason about classes of schedule types / processor models, we define the
    following properties that a processor model might possess. *)
 Section ProcessorModels.
-  (* Consider any job type and any processor state. *)
+  (** Consider any job type and any processor state. *)
   Context {Job : JobType}.
   Context {PState : Type}.
   Context `{ProcessorState Job PState}.
 
-  (* We say that a processor model provides unit service if no
+  (** We say that a processor model provides unit service if no
      job ever receives more than one unit of service at any time. *)
   Definition unit_service_proc_model :=
     forall (j : Job) (s : PState), service_in j s <= 1.
 
-  (* We say that a processor model offers ideal progress if a scheduled job
+  (** We say that a processor model offers ideal progress if a scheduled job
      always receives non-zero service. *)
   Definition ideal_progress_proc_model :=
     forall j s, scheduled_in j s -> service_in j s > 0.
 
-  (* In a uniprocessor model, the scheduled job is always unique. *)
+  (** In a uniprocessor model, the scheduled job is always unique. *)
   Definition uniprocessor_model :=
     forall j1 j2 s t,
       scheduled_at s j1 t ->
diff --git a/restructuring/model/readiness/basic.v b/restructuring/model/readiness/basic.v
index 6b16bfab608aa2a3890d74d855430156d441d287..47995a4ce57b99e0ccfa104f37b1881fa38556fb 100644
--- a/restructuring/model/readiness/basic.v
+++ b/restructuring/model/readiness/basic.v
@@ -1,29 +1,29 @@
 From rt.restructuring.behavior Require Export all.
 From rt.restructuring.analysis.basic_facts Require Import completion.
 
-(* We define the readiness indicator function for the classic Liu & Layland
+(** We define the readiness indicator function for the classic Liu & Layland
    model without jitter and no self-suspensions, where jobs are always
    ready. *)
 
 Section LiuAndLaylandReadiness.
-  (* Consider any kind of jobs... *)
+  (** Consider any kind of jobs... *)
   Context {Job : JobType}.
 
-  (* ... and any kind of processor state. *)
+  (** ... and any kind of processor state. *)
   Context {PState : Type}.
   Context `{ProcessorState Job PState}.
 
-  (* Supose jobs have an arrival time and a cost. *)
+  (** Supose jobs have an arrival time and a cost. *)
   Context `{JobArrival Job} `{JobCost Job}.
 
-  (* In the basic Liu & Layland model, a job is ready iff it is pending. *)
+  (** In the basic Liu & Layland model, a job is ready iff it is pending. *)
   Global Program Instance basic_ready_instance : JobReady Job PState :=
     {
       job_ready sched j t := pending sched j t
     }.
 
 
-  (* Under this definition, a schedule satisfies that only ready jobs execute
+  (** Under this definition, a schedule satisfies that only ready jobs execute
      as long as jobs must arrive to execute and completed jobs don't execute,
      which we note with the following theorem. *)
   Theorem basic_readiness_compliance:
diff --git a/restructuring/model/readiness/jitter.v b/restructuring/model/readiness/jitter.v
index a61b7a6b1637707bcf33ea4ccf7cb6b6216e28cb..f41420cf931c2fbe60cb176c1c85cb670b9bbfc9 100644
--- a/restructuring/model/readiness/jitter.v
+++ b/restructuring/model/readiness/jitter.v
@@ -3,28 +3,28 @@ From rt.restructuring.behavior Require Export all.
 
 From rt.util Require Import nat.
 
-(* We define the readiness indicator function for models with release jitter
+(** We define the readiness indicator function for models with release jitter
    (and no self-suspensions). *)
 
-(* Definition of a generic type of release jitter parameter. *)
+(** Definition of a generic type of release jitter parameter. *)
 Class JobJitter (Job : JobType) := job_jitter : Job -> duration.
 
 Section ReadinessOfJitteryJobs.
-  (* Consider any kind of jobs... *)
+  (** Consider any kind of jobs... *)
   Context {Job : JobType}.
 
-  (* ... and any kind of processor state. *)
+  (** ... and any kind of processor state. *)
   Context {PState : Type}.
   Context `{ProcessorState Job PState}.
 
-  (* Supose jobs have an arrival time, a cost, and a release jitter bound. *)
+  (** Supose jobs have an arrival time, a cost, and a release jitter bound. *)
   Context `{JobArrival Job} `{JobCost Job} `{JobJitter Job}.
 
-  (* We say that a job is released at a time after its arrival if the job's
+  (** We say that a job is released at a time after its arrival if the job's
      release jitter has passed. *)
   Definition is_released (j : Job) (t : instant) := job_arrival j + job_jitter j <= t.
 
-  (* A job that experiences jitter is ready only when the jitter-induced delay
+  (** A job that experiences jitter is ready only when the jitter-induced delay
      has passed after its arrival and if it is not yet complete. *)
   Global Program Instance jitter_ready_instance : JobReady Job PState :=
     {
diff --git a/restructuring/model/schedule/edf.v b/restructuring/model/schedule/edf.v
index 90c09b19f19baabd806e759bc71bf8ff64937ea6..8df42419536e8641bc3d1740bb633a62a54ee232 100644
--- a/restructuring/model/schedule/edf.v
+++ b/restructuring/model/schedule/edf.v
@@ -4,14 +4,14 @@ From rt.restructuring.behavior Require Export all.
 (** In this file, we define what it means to be an "EDF schedule". *)
 Section DefinitionOfEDF.
 
-  (* For any given type of jobs... *)
+  (** For any given type of jobs... *)
   Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
 
-  (* ... any given type of processor states: *)
+  (** ... any given type of processor states: *)
   Context {PState: eqType}.
   Context `{ProcessorState Job PState}.
 
-  (* We say that a schedule is locally an EDF schedule at a point in
+  (** We say that a schedule is locally an EDF schedule at a point in
      time [t] if the job scheduled at time [t] has a deadline that is
      earlier than or equal to the deadline of any other job that could
      be scheduled at time t but is scheduled later.
@@ -28,7 +28,7 @@ Section DefinitionOfEDF.
         job_arrival j' <= t ->
         job_deadline j <= job_deadline j'.
 
-  (* A schedule is an EDF schedule if it is locally EDF at every point in time. *)
+  (** A schedule is an EDF schedule if it is locally EDF at every point in time. *)
   Definition is_EDF_schedule (sched: schedule PState) := forall t, EDF_at sched t.
 
 End DefinitionOfEDF.
diff --git a/restructuring/model/schedule/priority_based/preemptive.v b/restructuring/model/schedule/priority_based/preemptive.v
index 2bfcdf195fbb284a49f7cf96367f9b048519214b..cd121cab66f6334e4d49a4a10d15b5f304c3cfa5 100644
--- a/restructuring/model/schedule/priority_based/preemptive.v
+++ b/restructuring/model/schedule/priority_based/preemptive.v
@@ -1,8 +1,8 @@
 From rt.restructuring.behavior Require Export all.
 From rt.restructuring.model Require Export priorities.
 
-(* We now define what it means for a schedule to respect a priority *)
-(* We only define it for a JLDP policy since the definitions for JLDP and JLFP are the same
+(** We now define what it means for a schedule to respect a priority *)
+(** We only define it for a JLDP policy since the definitions for JLDP and JLFP are the same
    and can be used through the conversions *)
 Section Priority.
   Context {Job: JobType} {Task: TaskType}.
diff --git a/restructuring/model/schedule/priority_based/priorities.v b/restructuring/model/schedule/priority_based/priorities.v
index c9dc439e5f85b70e0a2a5fc637b36a12971e7fc1..36e24cf6b9e47d809af39cf75d73ef026826a85a 100644
--- a/restructuring/model/schedule/priority_based/priorities.v
+++ b/restructuring/model/schedule/priority_based/priorities.v
@@ -2,19 +2,19 @@ From rt.restructuring.model Require Export task.
 From rt.util Require Export list.
 From mathcomp Require Export seq.
 
-(* Definitions of FP, JLFP and JLDP priority relations. *)
+(** Definitions of FP, JLFP and JLDP priority relations. *)
 
-(* In the following, "hep" means "higher or equal priority". We define an FP
+(** In the following, "hep" means "higher or equal priority". We define an FP
    policy as a relation among tasks, ... *)
 Class FP_policy (Task: TaskType) := hep_task : rel Task.
 
-(* ... a JLFP policy as a relation among jobs, a ... *)
+(** ... a JLFP policy as a relation among jobs, a ... *)
 Class JLFP_policy (Job: JobType) := hep_job : rel Job.
 
-(* ... a JLDP policy as a relation among jobs that may vary over time. *)
+(** ... a JLDP policy as a relation among jobs that may vary over time. *)
 Class JLDP_policy (Job: JobType) := hep_job_at : instant -> rel Job.
 
-(* Since FP policies are also JLFP and JLDP policies, we define
+(** Since FP policies are also JLFP and JLDP policies, we define
    conversions that express the generalization. *)
 Instance FP_to_JLFP (Job: JobType) (Task: TaskType)
          `{JobTask Job Task} `{FP_policy Task} : JLFP_policy Job :=
@@ -27,10 +27,10 @@ Section Priorities.
   Context {Job: eqType}.
 
   Section JLDP.
-    (* Consider any JLDP policy. *)
+    (** Consider any JLDP policy. *)
     Context `{JLDP_policy Job}.
 
-    (* We define common properties of the policy. Note that these definitions
+    (** We define common properties of the policy. Note that these definitions
        can also be used for JLFP and FP policies *)
     Definition reflexive_priorities := forall t, reflexive (hep_job_at t).
 
@@ -41,11 +41,11 @@ Section Priorities.
   End JLDP.
 
   Section FP.
-    (* Consider any FP policy. *)
+    (** Consider any FP policy. *)
     Context {Task : TaskType}.
     Context `{FP_policy Task}.
 
-    (* We define whether the policy is antisymmetric over a taskset ts. *)
+    (** We define whether the policy is antisymmetric over a taskset ts. *)
     Definition antisymmetric_over_taskset (ts : seq Task) :=
       antisymmetric_over_list hep_task ts.
   End FP.
diff --git a/restructuring/model/schedule/sequential.v b/restructuring/model/schedule/sequential.v
index 08c91c41b557d614b8e4132ab3435841329b6698..cc1d0235f548705eb6d4d281baefa61445848264 100644
--- a/restructuring/model/schedule/sequential.v
+++ b/restructuring/model/schedule/sequential.v
@@ -3,23 +3,23 @@ From rt.restructuring.model Require Export task.
 
 Section PropertyOfSequentiality.
 
-  (* Consider any type of job associated with any type of tasks... *)
+  (** Consider any type of job associated with any type of tasks... *)
   Context {Job : JobType}.
   Context {Task : TaskType}.
   Context `{JobTask Job Task}.
 
-  (* ... with arrival times and costs ... *)
+  (** ... with arrival times and costs ... *)
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
 
-  (* ... and any kind of processor state model. *)
+  (** ... and any kind of processor state model. *)
   Context {PState: Type}.
   Context `{ProcessorState Job PState}.
 
-  (* Given a schedule ... *)
+  (** Given a schedule ... *)
   Variable sched: schedule PState.
 
-  (* ...we say that jobs (or, rather, tasks) are sequential if each task's jobs
+  (** ...we say that jobs (or, rather, tasks) are sequential if each task's jobs
      are executed in the order they arrived. *)
   Definition sequential_jobs :=
     forall (j1 j2: Job) (t: instant),
diff --git a/restructuring/model/schedule/tdma/tdma.v b/restructuring/model/schedule/tdma/tdma.v
index 52fc166a10dd9e8d4aaf4951cd95bfc63bfc527d..08772bb06a273cd37e45b55c95aa6101ad022cfb 100644
--- a/restructuring/model/schedule/tdma/tdma.v
+++ b/restructuring/model/schedule/tdma/tdma.v
@@ -5,7 +5,7 @@ From mathcomp Require Export ssreflect ssrbool ssrfun eqtype ssrnat seq fintype
 (** In this section, we define the TDMA policy.*)
 Section TDMAPolicy.
 
-  (* The TDMA policy is based on two properties.
+  (** The TDMA policy is based on two properties.
       (1) Each task has a fixed, reserved time slot for execution;
       (2) These time slots are ordered in sequence to form a TDMA cycle, which repeats along the timeline.
       An example of TDMA schedule is illustrated in the following.
@@ -16,10 +16,10 @@ Section TDMAPolicy.
    *)
 
   Variable Task: eqType.
-  (* With each task, we associate the duration of the corresponding TDMA slot. *)
+  (** With each task, we associate the duration of the corresponding TDMA slot. *)
   Definition TDMA_slot := Task -> duration.
 
-  (* Moreover, within each TDMA cycle, task slots are ordered according to some relation.
+  (** Moreover, within each TDMA cycle, task slots are ordered according to some relation.
   (i.e, slot_order slot1 slot2 means that slot1 comes before slot2 in a TDMA cycle) *)
   Definition TDMA_slot_order := rel Task.
 
@@ -29,29 +29,29 @@ Class TDMAPolicy (T : TaskType) :=
   { task_time_slot : TDMA_slot T;
     slot_order : TDMA_slot_order T }.
 
-(* First, we define the properties of a valid TDMA policy. *)
+(** First, we define the properties of a valid TDMA policy. *)
 Section ValidTDMAPolicy.
 
   Context {Task : eqType}.
 
-  (* Consider any task set ts... *)
+  (** Consider any task set ts... *)
   Variable ts : {set Task}.
 
-  (* ...and a TDMA policy. *)
+  (** ...and a TDMA policy. *)
   Context `{TDMAPolicy Task}.
 
-  (* Time slot order must be transitive... *)
+  (** Time slot order must be transitive... *)
   Definition transitive_slot_order := transitive slot_order.
 
-  (* ..., totally ordered over the task set... *)
+  (** ..., totally ordered over the task set... *)
   Definition total_slot_order :=
     total_over_list slot_order ts.
 
-  (* ... and antisymmetric over task set. *)
+  (** ... and antisymmetric over task set. *)
   Definition antisymmetric_slot_order :=
     antisymmetric_over_list slot_order ts.
 
-  (* A valid time slot must be positive *)
+  (** A valid time slot must be positive *)
   Definition valid_time_slot :=
     forall tsk, tsk \in ts -> task_time_slot tsk > 0.
 
@@ -65,23 +65,23 @@ Section TDMADefinitions.
 
   Context {Task : eqType}.
 
-  (* Consider any task set ts... *)
+  (** Consider any task set ts... *)
   Variable ts : {set Task}.
 
-  (* ...and a TDMA policy. *)
+  (** ...and a TDMA policy. *)
   Context `{TDMAPolicy Task}.
 
-  (* We define the TDMA cycle as the sum of all the tasks' time slots *)
+  (** We define the TDMA cycle as the sum of all the tasks' time slots *)
   Definition TDMA_cycle:=
     \sum_(tsk <- ts) task_time_slot tsk.
 
-  (* We define the function returning the slot offset for each task:
+  (** We define the function returning the slot offset for each task:
          i.e., the distance between the start of the TDMA cycle and
          the start of the task time slot *)
   Definition task_slot_offset (tsk : Task) :=
     \sum_(prev_task <- ts | slot_order prev_task tsk && (prev_task != tsk)) task_time_slot prev_task.
 
-  (* The following function tests whether a task is in its time slot at instant t *)
+  (** The following function tests whether a task is in its time slot at instant t *)
   Definition task_in_time_slot (tsk : Task) (t:instant):=
     ((t + TDMA_cycle - (task_slot_offset tsk)%% TDMA_cycle) %% TDMA_cycle)
     < (task_time_slot tsk).
@@ -93,28 +93,28 @@ Section TDMASchedule.
 
   Context `{JobArrival Job} `{JobCost Job} `{JobReady Job (option Job)} `{JobTask Job Task}.
 
-  (* Consider any job arrival sequence... *)
+  (** Consider any job arrival sequence... *)
   Variable arr_seq : arrival_sequence Job.
 
-  (* ..., any uniprocessor ideal schedule ... *)
+  (** ..., any uniprocessor ideal schedule ... *)
   Variable sched : schedule (option Job).
 
-  (* ... and any sporadic task set. *)
+  (** ... and any sporadic task set. *)
   Variable ts: {set Task}.
 
   Context `{TDMAPolicy Task}.
 
-  (* In order to characterize a TDMA policy, we first define whether a job is executing its TDMA slot at time t. *)
+  (** In order to characterize a TDMA policy, we first define whether a job is executing its TDMA slot at time t. *)
   Definition job_in_time_slot (job:Job) (t:instant):=
     task_in_time_slot ts (job_task job) t.
 
-  (* We say that a TDMA policy is respected by the schedule iff
+  (** We say that a TDMA policy is respected by the schedule iff
        1. when a job is scheduled at time t, then the corresponding task
           is also in its own time slot... *)
   Definition sched_implies_in_slot j t:=
     scheduled_at sched j t -> job_in_time_slot j t.
 
-  (* 2. when a job is backlogged at time t,the corresponding task
+  (** 2. when a job is backlogged at time t,the corresponding task
           isn't in its own time slot or another previous job of the same task is scheduled *)
   Definition backlogged_implies_not_in_slot_or_other_job_sched j t:=
     backlogged sched j t ->
diff --git a/restructuring/model/schedule/tdma/tdma_facts.v b/restructuring/model/schedule/tdma/tdma_facts.v
index f9578fe8167057be619d40efec85f8530008bb51..b07b751324ec655b9303ae67087518a848403756 100644
--- a/restructuring/model/schedule/tdma/tdma_facts.v
+++ b/restructuring/model/schedule/tdma/tdma_facts.v
@@ -5,22 +5,22 @@ From rt.util Require Import all.
 Section TDMAFacts.
   Context {Task:eqType}.
 
-  (* Consider any task set ts... *)
+  (** Consider any task set ts... *)
   Variable ts: {set Task}.
 
-  (* ... with a TDMA policy *)
+  (** ... with a TDMA policy *)
   Context `{TDMAPolicy Task}.
 
   Section TimeSlotFacts.
-    (* Consider any task in ts*)
+    (** Consider any task in ts*)
     Variable task: Task.
     Hypothesis H_task_in_ts: task \in ts.
 
-    (* Assume task_time_slot is valid time slot*)
+    (** Assume task_time_slot is valid time slot*)
     Hypothesis time_slot_positive:
       valid_time_slot ts.
 
-    (* Obviously, the TDMA cycle is greater or equal than any task time slot which is
+    (** Obviously, the TDMA cycle is greater or equal than any task time slot which is
           in TDMA cycle *)
     Lemma TDMA_cycle_ge_each_time_slot:
       TDMA_cycle ts >= task_time_slot task.
@@ -30,14 +30,14 @@ Section TDMAFacts.
         by apply leqnn.
     Qed.
 
-    (* Thus, a TDMA cycle is always positive *)
+    (** Thus, a TDMA cycle is always positive *)
     Lemma TDMA_cycle_positive:
       TDMA_cycle ts > 0.
     Proof.
       move:time_slot_positive=>/(_ task H_task_in_ts)/leq_trans;apply;apply TDMA_cycle_ge_each_time_slot.
     Qed.
 
-    (* Slot offset is less then cycle *)
+    (** Slot offset is less then cycle *)
     Lemma Offset_lt_cycle:
       task_slot_offset ts task < TDMA_cycle ts.
     Proof.
@@ -50,7 +50,7 @@ Section TDMAFacts.
         easy.
     Qed.
 
-    (* For a task, the sum of its slot offset and its time slot is
+    (** For a task, the sum of its slot offset and its time slot is
           less then or equal to cycle. *)
     Lemma Offset_add_slot_leq_cycle:
       task_slot_offset ts task + task_time_slot task <= TDMA_cycle ts.
@@ -65,17 +65,17 @@ Section TDMAFacts.
     Qed.
   End TimeSlotFacts.
 
-  (* Now we prove that no two tasks share the same time slot at any time. *)
+  (** Now we prove that no two tasks share the same time slot at any time. *)
   Section TimeSlotOrderFacts.
-    (* Consider any task in ts*)
+    (** Consider any task in ts*)
     Variable task: Task.
     Hypothesis H_task_in_ts: task \in ts.
 
-    (* Assume task_time_slot is valid time slot*)
+    (** Assume task_time_slot is valid time slot*)
     Hypothesis time_slot_positive:
       valid_time_slot ts.
 
-    (* Assume that slot order is total... *)
+    (** Assume that slot order is total... *)
     Hypothesis slot_order_total:
       total_slot_order ts.
 
@@ -87,7 +87,7 @@ Section TDMAFacts.
     Hypothesis slot_order_transitive:
       transitive_slot_order.
 
-    (* Then, we can prove that the difference value between two offsets is
+    (** Then, we can prove that the difference value between two offsets is
         at least a slot *)
     Lemma relation_offset:
       forall tsk1 tsk2, tsk1 \in ts ->
@@ -113,7 +113,7 @@ Section TDMAFacts.
         intros* T. case(i!=tsk1);case (slot_order i tsk2);case (i!=tsk2) ;auto.
     Qed.
 
-    (* Then, we proved that no two tasks share the same time slot at any time. *)
+    (** Then, we proved that no two tasks share the same time slot at any time. *)
     Lemma task_in_time_slot_uniq:
       forall tsk1 tsk2 t, tsk1 \in ts -> task_time_slot tsk1 > 0 ->
                                    tsk2 \in ts -> task_time_slot tsk2 > 0 ->
diff --git a/restructuring/model/schedule/work_conserving.v b/restructuring/model/schedule/work_conserving.v
index e5447011b7b26907ffe999662e7b44b428e8ccf8..3fea9faf808c21b7af02ce68231900e261e062e8 100644
--- a/restructuring/model/schedule/work_conserving.v
+++ b/restructuring/model/schedule/work_conserving.v
@@ -1,6 +1,6 @@
 From rt.restructuring.behavior Require Export all.
 
-(* In this file, we introduce a restrictive definition of work conserving
+(** In this file, we introduce a restrictive definition of work conserving
    uniprocessor schedules. The definition is restrictive because it does not
    allow for effects such as jitter or self-suspensions that affect whether a
    job can be scheduled at a given point in time. A more general notion of work
@@ -8,25 +8,25 @@ From rt.restructuring.behavior Require Export all.
    global scheduling, is TBD. *)
 
 Section WorkConserving.
-  (* Consider any type of job associated with any type of tasks... *)
+  (** Consider any type of job associated with any type of tasks... *)
   Context {Job: JobType}.
 
-  (* ... with arrival times and costs ... *)
+  (** ... with arrival times and costs ... *)
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
 
-  (* ... and any kind of processor state model. *)
+  (** ... and any kind of processor state model. *)
   Context {PState: Type}.
   Context `{ProcessorState Job PState}.
 
-  (* Further, allow for any notion of job readiness. *)
+  (** Further, allow for any notion of job readiness. *)
   Context `{JobReady Job PState}.
 
-  (* Given an arrival sequence and a schedule ... *)
+  (** Given an arrival sequence and a schedule ... *)
   Variable arr_seq : arrival_sequence Job.
   Variable sched: schedule PState.
 
-  (* We say that a scheduler is work-conserving iff whenever a job j
+  (** We say that a scheduler is work-conserving iff whenever a job j
      is backlogged, the processor is always busy with another job. *)
   Definition work_conserving :=
     forall j t,
diff --git a/restructuring/model/task.v b/restructuring/model/task.v
index f25bdb465f277ebdee5d20dc8e427d3cc24c4ad2..ed2780b489c0954930cb1e2baae846c0b229d2c6 100644
--- a/restructuring/model/task.v
+++ b/restructuring/model/task.v
@@ -1,44 +1,44 @@
 From mathcomp Require Export ssrbool.
 From rt.restructuring.behavior Require Export all.
   
-(* Throughout the library we assume that tasks have decidable equality *)
+(** Throughout the library we assume that tasks have decidable equality *)
 Definition TaskType := eqType.
 
-(* Definition of a generic type of parameter relating jobs to tasks *)
+(** Definition of a generic type of parameter relating jobs to tasks *)
 Class JobTask (Job : JobType) (Task : TaskType) := job_task : Job -> Task.
 
-(* Definition of a generic type of parameter for task deadlines *)
+(** Definition of a generic type of parameter for task deadlines *)
 Class TaskDeadline (Task : TaskType) := task_deadline : Task -> duration.
 
-(* Definition of a generic type of parameter for task cost *)
+(** Definition of a generic type of parameter for task cost *)
 Class TaskCost (Task : TaskType) := task_cost : Task -> duration.
 
-(* Definition of a generic type of parameter relating tasks 
+(** Definition of a generic type of parameter relating tasks 
    to the length of the maximum nonpreeptive segment. *)
 Class TaskMaxNonpreemptiveSegment (Task : TaskType) :=
   task_max_nonpreeptive_segment : Task -> duration.
 
-(* Definition of a generic type of parameter relating tasks
+(** Definition of a generic type of parameter relating tasks
    to theirs run-to-completion threshold. *)
 Class TaskRunToCompletionThreshold (Task : TaskType) :=
   task_run_to_completion_threshold : Task -> duration.
 
 Section SameTask.
   
-  (* For any type of job associated with any type of tasks... *)
+  (** For any type of job associated with any type of tasks... *)
   Context {Job : JobType}.
   Context {Task : TaskType}.
   Context `{JobTask Job Task}.
 
-  (* ... we say that two jobs j1 and j2 are from the same task iff job_task j1 is equal to job_task j2, ... *)
+  (** ... we say that two jobs j1 and j2 are from the same task iff job_task j1 is equal to job_task j2, ... *)
   Definition same_task (j1 j2 : Job) := job_task j1 == job_task j2.
   
-  (* ... we also say that job j is a job of task tsk iff job_task j is equal to tsk. *)
+  (** ... we also say that job j is a job of task tsk iff job_task j is equal to tsk. *)
   Definition job_of_task (tsk : Task) (j : Job) := job_task j == tsk.
 
 End SameTask.
 
-(* Given task deadlines and a mapping from jobs to tasks we provide a generic definition of job_deadline *)
+(** 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)
          `{TaskDeadline Task} `{JobArrival Job} `{JobTask Job Task} : JobDeadline Job :=
@@ -46,59 +46,59 @@ Instance job_deadline_from_task_deadline
 
 
 
-(* In this section, we introduce properties of a task. *)
+(** In this section, we introduce properties of a task. *)
 Section PropertesOfTask.
 
-  (* Consider any type of tasks. *)
+  (** Consider any type of tasks. *)
   Context {Task : TaskType}.
   Context `{TaskCost Task}.
   Context `{TaskDeadline Task}.
 
-  (* Next we intrdoduce attributes of a valid sporadic task. *)
+  (** Next we intrdoduce attributes of a valid sporadic task. *)
   Section ValidTask.
     
-    (* Consider an arbitrary task. *)
+    (** Consider an arbitrary task. *)
     Variable tsk: Task.
     
-    (* The cost and deadline of the task must be positive. *)
+    (** The cost and deadline of the task must be positive. *)
     Definition task_cost_positive := task_cost tsk > 0.
     Definition task_deadline_positive := task_deadline tsk > 0.
 
-    (* The task cost cannot be larger than the deadline or the period. *)
+    (** The task cost cannot be larger than the deadline or the period. *)
     Definition task_cost_le_deadline := task_cost tsk <= task_deadline tsk.
     
   End ValidTask.
   
-  (* Job of task *)
+  (** Job of task *)
   Section ValidJobOfTask.
     
-    (* Consider any type of jobs associated with the tasks ... *)
+    (** Consider any type of jobs associated with the tasks ... *)
     Context {Job : JobType}.
     Context `{JobTask Job Task}.
     Context `{JobCost Job}.
     Context `{JobDeadline Job}.
 
-    (* Consider an arbitrary job. *)
+    (** Consider an arbitrary job. *)
     Variable j: Job.
 
-    (* The job cost cannot be larger than the task cost. *)
+    (** The job cost cannot be larger than the task cost. *)
     Definition job_cost_le_task_cost :=
       job_cost j <= task_cost (job_task j).
 
   End ValidJobOfTask.
 
-  (* Jobs of task *)
+  (** Jobs of task *)
   Section ValidJobsTask.
           
-    (* Consider any type of jobs associated with the tasks ... *)
+    (** Consider any type of jobs associated with the tasks ... *)
     Context {Job : JobType}.
     Context `{JobTask Job Task}.
     Context `{JobCost Job}.
     
-    (* ... and any arrival sequence. *)
+    (** ... and any arrival sequence. *)
     Variable arr_seq : arrival_sequence Job.
 
-    (* The cost of a job from the arrival sequence cannot
+    (** The cost of a job from the arrival sequence cannot
        be larger than the task cost. *)
     Definition cost_of_jobs_from_arrival_sequence_le_task_cost :=
       forall j,
@@ -109,31 +109,31 @@ Section PropertesOfTask.
 
 End PropertesOfTask.
 
-(* In this section, we introduce properties of a task set. *)
+(** In this section, we introduce properties of a task set. *)
 Section PropertesOfTaskSet.
 
-  (* Consider any type of tasks ... *)
+  (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
   Context `{TaskCost Task}.
 
-  (*  ... and any type of jobs associated with these tasks ... *)
+  (**  ... and any type of jobs associated with these tasks ... *)
   Context {Job : JobType}.
   Context `{JobTask Job Task}.
   Context `{JobCost Job}.
 
-  (* ... and any arrival sequence. *)
+  (** ... and any arrival sequence. *)
   Variable arr_seq : arrival_sequence Job.
 
-  (* Consider an arbitrary task set. *)
+  (** Consider an arbitrary task set. *)
   Variable ts : seq Task.
 
-  (* Tasks from the task set have a positive cost. *)
+  (** Tasks from the task set have a positive cost. *)
   Definition tasks_cost_positive :=
     forall tsk,
       tsk \in ts ->
       task_cost_positive tsk. 
 
-  (* All jobs in the arrival sequence come from the taskset. *)
+  (** All jobs in the arrival sequence come from the taskset. *)
   Definition all_jobs_from_taskset :=
     forall j,
       arrives_in arr_seq j ->