fix match_states

1 files changed, 8 insertions, 6 deletions

diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index 2116ac70..ed661280 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -6,7 +6,7 @@ Require Import Errors Linking RTLtoBTL.
 
 Require Import Linking.
 
-Record match_function dupmap f tf: Prop := {
+Record match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := {
   dupmap_correct: match_cfg dupmap (fn_code tf) (RTL.fn_code f);
   dupmap_entrypoint: dupmap!(fn_entrypoint tf) = Some (RTL.fn_entrypoint f);
   code_right_assoc: forall pc ib, (fn_code tf)!pc=Some ib -> is_right_assoc ib.(entry);
@@ -80,25 +80,27 @@ Let tge := Genv.globalenv tprog.
 
 Local Open Scope nat_scope.
 
-(* TODO: 
-  faire un dessin ASCII art de la simulation avec match_states_intro 
+(* TODO:
 
 Le (option iblock) en paramètre représente l'état de l'exécution côté BTL 
 depuis le début de l'exécution du block
+
+  faire un dessin ASCII art de la simulation avec match_states_intro 
+
 *)
 
 Inductive match_states: (option iblock) -> RTL.state -> state -> Prop :=
   | match_states_intro (* TODO: LES DETAILS SONT SANS DOUTE A REVOIR !!! *)
-      ib dupmap st f sp pc rs m st' f' pc' pc0' pc0 rs0 m0 isfst ib0
+      ib dupmap st f sp pc rs m st' f' pc0' pc0 rs0 m0 isfst ib0
       (STACKS: list_forall2 match_stackframes st st')
       (TRANSF: match_function dupmap f f')
       (ATpc0: (fn_code f')!pc0' = Some ib0)
       (DUPLIC: dupmap!pc0' = Some pc0)
-      (MIB: match_iblock dupmap (RTL.fn_code f) isfst pc' ib None)
+      (MIB: match_iblock dupmap (RTL.fn_code f) isfst pc ib None)
       (RIGHTA: is_right_assoc ib)
       (RTL_RUN: star RTL.step ge (RTL.State st f sp pc0 rs0 m0) E0 (RTL.State st f sp pc rs m))
       (BTL_RUN: iblock_istep_run tge sp ib0.(entry) rs0 m0 = iblock_istep_run tge sp ib rs m)
-      : match_states (Some ib) (RTL.State st f sp pc rs m) (State st' f' sp pc' rs m)
+      : match_states (Some ib) (RTL.State st f sp pc rs m) (State st' f' sp pc0' rs0 m0)
   | match_states_call
       st st' f f' args m
       (STACKS: list_forall2 match_stackframes st st')