Improving the coqdoc

1 files changed, 15 insertions, 8 deletions

diff --git a/kvx/Asmblockdeps.v b/kvx/Asmblockdeps.v
index 1881e7e9..3d981100 100644
--- a/kvx/Asmblockdeps.v
+++ b/kvx/Asmblockdeps.v
@@ -12,12 +12,14 @@
 (*                                                             *)
 (* *************************************************************)
 
-(** * Translation from Asmblock to AbstractBB 
+(** * Translation from [Asmvliw] to [AbstractBB] *)
 
-    We define a specific instance of AbstractBB, named L, translate bblocks from Asmblock into this instance
-    AbstractBB will then define two semantics for L : a sequential, and a semantic one
-    We prove a bisimulation between the parallel semantics of L and AsmVLIW
-    From this, we also deduce a bisimulation between the sequential semantics of L and Asmblock *)
+(** We define a specific instance [L] of [AbstractBB] and translate [bblocks] from [Asmvliw] into [L].
+    [AbstractBB] will then define two semantics for [L]: a sequential and a parallel one.
+    We prove a bisimulation between the parallel semantics of [L] and [AsmVLIW].
+    We also prove a bisimulation between the sequential semantics of [L] and [Asmblock].
+    Then, the checkers on [Asmblock] and [Asmvliw] are deduced from those of [L].
+ *)
 
 Require Import AST.
 Require Import Asmblock.
@@ -40,7 +42,7 @@ Require Import Lia.
 
 Open Scope impure.
 
-(** Definition of L *)
+(** Definition of [L] *)
 
 Module P<: ImpParam.
 Module R := Pos.
@@ -660,7 +662,7 @@ Module IST := ImpSimu L ImpPosDict.
 Import L.
 Import P.
 
-(** Compilation from Asmblock to L *)
+(** Compilation from [Asmvliw] to [L] *)
 
 Local Open Scope positive_scope.
 
@@ -748,6 +750,8 @@ Definition inv_ppos (p: R.t) : option preg :=
 
 Notation "a @ b" := (Econs a b) (at level 102, right associativity).
 
+(** Translations of instructions *)
+
 Definition trans_control (ctl: control) : inst :=
   match ctl with
   | Pret => [(#PC, PReg(#RA))]
@@ -859,6 +863,8 @@ Proof.
   intros. destruct bb as [hdr bdy ex COR]; unfold no_header; simpl. unfold trans_block. simpl. reflexivity.
 Qed.
 
+(** Lemmas on the translation *)
+
 Definition state := L.mem.
 Definition exec := L.run.
 
@@ -1800,6 +1806,7 @@ Definition bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock) : ?? bool :=
 
 Local Hint Resolve IST.bblock_simu_test_correct bblock_simu_reduce IST.verb_bblock_simu_test_correct: wlp.
 
+(** Main simulation (Impure) theorem *) 
 Theorem bblock_simu_test_correct verb p1 p2 :
   WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn, Asmblockprops.bblock_simu ge fn p1 p2.
 Proof.
@@ -1807,7 +1814,7 @@ Proof.
 Qed.
 Hint Resolve bblock_simu_test_correct: wlp.
 
-(* Coerce bblock_simu_test into a pure function (this is a little unsafe like all oracles in CompCert). *)
+(** ** Coerce bblock_simu_test into a pure function (this is a little unsafe like all oracles in CompCert). *)
 
 Import UnsafeImpure.