Improving the coqdoc

1 files changed, 9 insertions, 4 deletions

diff --git a/kvx/lib/Machblockgen.v b/kvx/lib/Machblockgen.v
index 287e4f7b..ab186083 100644
--- a/kvx/lib/Machblockgen.v
+++ b/kvx/lib/Machblockgen.v
@@ -29,6 +29,8 @@ Require Import Mach.
 Require Import Linking.
 Require Import Machblock.
 
+(** * Tail-recursive (greedy) translation from Mach code to Machblock code *)
+
 Inductive Machblock_inst: Type :=
 | MB_label (lbl: label) 
 | MB_basic (bi: basic_inst)
@@ -71,9 +73,12 @@ Definition add_to_new_bblock (i:Machblock_inst) : bblock :=
   | MB_cfi i => cfi_bblock i
   end.
 
-(** Adding an instruction to the beginning of a bblock list
-  * Either adding the instruction to the head of the list,
-  * or create a new bblock with the instruction *)
+(** Adding an instruction to the beginning of a bblock list by
+
+- either adding the instruction to the head of the list,
+
+- or creating a new bblock with the instruction 
+*)
 Definition add_to_code (i:Machblock_inst) (bl:code) : code :=
   match bl with
   | bh::bl0 => match i with
@@ -112,7 +117,7 @@ Definition transf_program (src: Mach.program) : program :=
   transform_program transf_fundef src.
 
 
-(** Abstracting trans_code *)
+(** * Abstracting trans_code with a simpler inductive relation *)
 
 Inductive is_end_block: Machblock_inst -> code -> Prop :=
   | End_empty mbi: is_end_block mbi nil