Cleanup last commit : deleted unused definitions, Cmds_PRE_ok definition updated.

coq/Commands.v

@@ -76,7 +76,7 @@ Section Commands.
 
   Definition isPRE (cmd : Command_t) :=
     cmd.(CKind) == PRE.
-    
+
   Definition PRE_of_req req t :=
     mkCmd t PRE req.
 

coq/Trace.v

@@ -8,9 +8,6 @@ Section Trace.
   Definition Same_Bank (a b : Command_t) :=
     a.(Request).(Bank) == b.(Request).(Bank).
 
-  Definition Same_Bank_3 (a b c : Command_t) :=
-    Same_Bank a b && Same_Bank a c.
-
   Definition ACT_to_ACT (a b : Command_t) :=
     isACT a && isACT b.
 
@@ -44,7 +41,7 @@ Section Trace.
 
     (* Between any two PREs to the same bank, there has to be an ACT to the same bank in between *)
     Cmds_PRE_ok : forall a b, a \in Commands -> b \in Commands ->
-                  PRE_to_PRE a b -> Same_Bank a b -> a != b -> 
+                  PRE_to_PRE a b -> Same_Bank a b -> Before a b -> 
                   exists c : Command_t, isACT c /\ Same_Bank a c /\ c \in Between Commands a b;
 
     (* Ensure that the time between two ACT commands respects T_RC *)