debroussaillage et precisions...

1 files changed, 15 insertions, 15 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 8529010c..28941e01 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -292,26 +292,26 @@ Definition iblock_step stack f sp rs m ib t s: Prop :=
   of system calls performed during this transition. *)
 
 Inductive step: state -> trace -> state -> Prop :=
-  | exec_iblock stack ib f sp pc rs m t s:
-      (fn_code f)!pc = Some ib ->
-      iblock_step stack f sp rs m ib.(entry) t s ->
-      step (State stack f sp pc rs m) t s
-  | exec_function_internal stack f args m m' stk:
-      Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
-      step (Callstate stack (Internal f) args m)
-        E0 (State stack
+  | exec_iblock stack ib f sp pc rs m t s
+      (PC: (fn_code f)!pc = Some ib)
+      (STEP: iblock_step stack f sp rs m ib.(entry) t s)
+      :step (State stack f sp pc rs m) t s
+  | exec_function_internal stack f args m m' stk
+      (ALLOC: Mem.alloc m 0 f.(fn_stacksize) = (m', stk))
+      :step (Callstate stack (Internal f) args m)
+         E0 (State stack
                   f
                   (Vptr stk Ptrofs.zero)
                   f.(fn_entrypoint)
                   (init_regs args f.(fn_params))
                   m')
-  | exec_function_external stack ef args res t m m':
-      external_call ef ge args m t res m' ->
-      step (Callstate stack (External ef) args m)
-         t (Returnstate stack res m')
-  | exec_return stack res f sp pc rs vres m:
-      step (Returnstate (Stackframe res f sp pc rs :: stack) vres m)
-        E0 (State stack f sp pc (rs#res <- vres) m)
+  | exec_function_external stack ef args res t m m'
+      (EXTCALL: external_call ef ge args m t res m')
+      :step (Callstate stack (External ef) args m)
+          t (Returnstate stack res m')
+  | exec_return stack res f sp pc rs vres m
+      :step (Returnstate (Stackframe res f sp pc rs :: stack) vres m)
+         E0 (State stack f sp pc (rs#res <- vres) m)
 .
 
 End RELSEM.