Improving the coqdoc

1 files changed, 7 insertions, 12 deletions

diff --git a/kvx/PostpassScheduling.v b/kvx/PostpassScheduling.v
index 7518866d..1f1f238a 100644
--- a/kvx/PostpassScheduling.v
+++ b/kvx/PostpassScheduling.v
@@ -12,6 +12,8 @@
 (*                                                             *)
 (* *************************************************************)
 
+(** Implementation (and basic properties) of the verified postpass scheduler *)
+
 Require Import Coqlib Errors AST Integers.
 Require Import Asmblock Axioms Memory Globalenvs.
 Require Import Asmblockdeps Asmblockgenproof0 Asmblockprops.
@@ -19,20 +21,13 @@ Require Peephole.
 
 Local Open Scope error_monad_scope.
 
-(** Oracle taking as input a basic block,
-    returns a schedule expressed as a list of bundles *)
+(** * Oracle taking as input a basic block,
+    returns a scheduled list of bundles *)
 Axiom schedule: bblock -> (list (list basic)) * option control.
 
 Extract Constant schedule => "PostpassSchedulingOracle.schedule".
 
-Definition state' := L.mem.
-Definition outcome' := option state'.
-
-Definition bblock' := L.bblock.
-
-Definition exec' := L.run.
-
-Definition exec := exec_bblock.
+(** * Concat all bundles into one big basic block *)
 
 (* Lemmas necessary for defining concat_all *)
 Lemma app_nonil {A: Type} (l l': list A) : l <> nil -> l ++ l' <> nil.
@@ -49,8 +44,6 @@ Proof.
   - intros. rewrite <- app_comm_cons. discriminate.
 Qed.
 
-
-
 Definition check_size bb :=
   if zlt Ptrofs.max_unsigned (size bb)
     then Error (msg "PostpassSchedulingproof.check_size")
@@ -213,6 +206,8 @@ Qed.
 Inductive is_concat : bblock -> list bblock -> Prop :=
   | mk_is_concat: forall tbb lbb, concat_all lbb = OK tbb -> is_concat tbb lbb.
 
+(** * Remainder of the verified scheduler *)
+
 Definition verify_schedule (bb bb' : bblock) : res unit :=
   match bblock_simub bb bb' with
   | true => OK tt