diff --git a/link/README.md b/link/README.md
index 8b71be9d72ba44e45889cb70f8cd4214f094c58e..fdb7011af759d03c60158dcc5332ae67461f6096 100644
--- a/link/README.md
+++ b/link/README.md
@@ -40,3 +40,14 @@ make
 ```
 
 to compile everything.
+
+Documentation
+-------------
+
+To generate the documentation
+
+```shell
+make html
+```
+
+The file `html/toc.html` can then be opened with any browser.
diff --git a/link/clock.v b/link/clock.v
index fc8f8b55cb17d24dbcfa852361cd1b16da29a82b..f3388567150f10cf43a3b22991ff124b937e8d0a 100644
--- a/link/clock.v
+++ b/link/clock.v
@@ -15,7 +15,7 @@ Import Order.Theory GRing.Theory Num.Theory.
 (** time is nat, let's define universal_time as non negative reals *)
 Definition universal_time := {nonneg R}.
 
-(** ** Definitions of [uclock] and reverse function [next_tick] *)
+(** * Definitions of [uclock] and reverse function [next_tick] *)
 
 Record uclock := {
   (** A universal clock is just a function from clock tick indexes (time := nat)
@@ -77,7 +77,7 @@ Qed.
 Definition next_tick (c : uclock) (r : universal_time) : instant :=
   proj1_sig (next_tick_ex c r).
 
-(** ** Some properties on clocks *)
+(** * Some properties on clocks *)
 
 Lemma uclock_next_tick_gt (c : uclock) (t : universal_time) :
   t%:nngnum <= (c (next_tick c t))%:nngnum.
@@ -188,7 +188,7 @@ rewrite ler_subl_addl; apply: (le_trans dlem).
 by rewrite -add1n PoszD intrD mulrDr mulr1.
 Qed.
 
-(** ** A few specific clocks *)
+(** * A few specific clocks *)
 
 (** Pseudo periodic clocks: clocks whose time between ticks is not
     necessarily exactly the same but might be n an interval
diff --git a/link/delay.v b/link/delay.v
index b67fea20e91e97470107f1ef510c90e5aa89ce81..68c6babc4959a9816686983c6dec057e37b4cd8a 100644
--- a/link/delay.v
+++ b/link/delay.v
@@ -30,7 +30,6 @@ Context {PState : ProcessorState Job}.
 Context {jr : JobReady Job PState}.
 Variable sched : schedule PState.
 
-(* TODO: hypothèse peu courante ? *)
 Hypothesis H_job_cost_positive : forall j, job_cost_positive j.
 
 (** * First consider only a single job *)
@@ -268,8 +267,8 @@ Lemma task_response_time_of_hDev (tsk : Task) (c : uclock)
       A D d :
   related_arrival_flow_cc c tsk arr_seq A ->
   related_arrival_flow_cc c tsk (completion_sequence arr_seq sched) D ->
-  (* we must assume FIFO inside the task (for network calculus
-     says nothing about individual jobs in sequences) *)
+  (** we must assume FIFO inside the task (for network calculus
+      says nothing about individual jobs in sequences) *)
   FIFO_arrival_sequence sched arr_seq tsk tsk ->
   ((hDev A D)%:nngenum <= (d%:R * (uclock_min_intertick c)%:num)%:E)%E ->
   task_response_time_bound arr_seq sched tsk d.
diff --git a/link/fifo.v b/link/fifo.v
index 25454136f7a0f119378420c1021af7da441c8f72..8819c8c2bdd665844ac5d4b54d1d73f0790fa6c2 100644
--- a/link/fifo.v
+++ b/link/fifo.v
@@ -143,8 +143,8 @@ exact/mem_bigcat_nat/(leq_ltn_trans Ht'''').
 Qed.
 
 Lemma FIFO_flow_cc_to_arrival_sequences (c : uclock) :
-  (* we must assume FIFO inside each sequence (for network calculus
-     says nothing about individual jobs in sequences) *)
+  (** we must assume FIFO inside each sequence (for network calculus
+      says nothing about individual jobs in sequences) *)
   (forall tsk, FIFO_arrival_sequence arr tsk tsk) ->
   let A := flow_cc_of_arrival_sequence arr c in
   let D := flow_cc_of_arrival_sequence (completion_sequence arr sched) c in
diff --git a/link/static_priority.v b/link/static_priority.v
index 81f283dab102819b906666c800b351c8b3483c15..c2d01b4ec9bbe8c10c5c4e5b263c3beca40971b3 100644
--- a/link/static_priority.v
+++ b/link/static_priority.v
@@ -220,9 +220,9 @@ rewrite /scheduled_at !scheduled_in_def => /eqP-> /eqP[] jj'.
 by move: priorts; apply/negP; rewrite -leqNgt -jtsk -j'ts jj'.
 Qed.
 
-(* The other direction doesn't hold because we only register
-   completion of jobs, so we can't guarantee that the fixed priority policy
-   is respected at each instant of job executions. *)
+(** The other direction doesn't hold because we only register
+    completion of jobs, so we can't guarantee that the fixed priority policy
+    is respected at each instant of job executions. *)
 Lemma FP_flow_cc_to_arrival_sequences (c : uclock) :
   (* we must assume FIFO inside each sequence (for network calculus
      says nothing about individual jobs in sequences) *)