Merge branch 'mppa-RTLpathSE-verif-hash-junk' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-RTLpathSE-verif-hash-junk

1 files changed, 12 insertions, 13 deletions

diff --git a/kvx/abstractbb/Parallelizability.v b/kvx/abstractbb/Parallelizability.v
index feebeee5..79ec9038 100644
--- a/kvx/abstractbb/Parallelizability.v
+++ b/kvx/abstractbb/Parallelizability.v
@@ -26,7 +26,7 @@ Require Import Sorting.Permutation.
 Require Import Bool.
 Local Open Scope lazy_bool_scope.
 
-
+(** * Definition of the parallel semantics *)
 Module ParallelSemantics (L: SeqLanguage).
 
 Export L.
@@ -590,17 +590,17 @@ End PARALLELI.
 End ParallelizablityChecking.
 
 
-Module Type PseudoRegSet.
-
-Declare Module R: PseudoRegisters.
-
-(** We assume a datatype [t] refining (list R.t)
+(** * We assume a datatype [PseudoRegSet.t] refining [list R.t] *)
 
+(** 
 This data-refinement is given by an abstract "invariant" match_frame below, 
 preserved by the following operations.
-
 *)
 
+Module Type PseudoRegSet.
+
+Declare Module R: PseudoRegisters.
+
 Parameter t: Type.
 Parameter match_frame: t -> (list R.t) -> Prop.
 
@@ -716,6 +716,11 @@ End ParallelChecks.
 
 
 
+(** * Implementing the datatype [PosPseudoRegSet.t] refining [list R.t] *)
+
+(* This data-refinement is given by an abstract "invariant" match_frame below, 
+preserved by the following operations.
+*)
 
 Require Import PArith.
 Require Import MSets.MSetPositive.
@@ -724,12 +729,6 @@ Module PosPseudoRegSet <: PseudoRegSet with Module R:=Pos.
 
 Module R:=Pos.
 
-(** We assume a datatype [t] refining (list R.t)
-
-This data-refinement is given by an abstract "invariant" match_frame below, 
-preserved by the following operations.
-
-*)
 
 Definition t:=PositiveSet.t.