avancement ref de l'exe symbolique

1 files changed, 4 insertions, 7 deletions

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 4b4571e4..464bb0f0 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -630,7 +630,7 @@ Qed.
 Fixpoint transfer_sreg (inputs: list reg) (sreg: reg -> sval): reg -> sval :=
   match inputs with
   | nil => fun r => Sundef 
-  | r1::l => fun r => if Pos.eq_dec r r1 then sreg r1 else transfer_sreg l sreg r
+  | r1::l => fun r => if Pos.eq_dec r1 r then sreg r1 else transfer_sreg l sreg r
   end.
 
 Definition str_inputs (f:function) (tbl: list exit) (or:option reg) := transfer_sreg (Regset.elements (pre_inputs f tbl or)).
@@ -655,15 +655,12 @@ Definition tr_sis f (fi: final) (sis: sistate) :=
      si_sreg := poly_tr str_inputs f fi sis.(si_sreg); 
      si_smem := sis.(si_smem) |}.
 
-Definition sreg_eval ctx (sis: sistate) (r: reg): option val :=
-  eval_sval ctx (sis.(si_sreg) r).
-
 Lemma tr_sis_regs_correct_aux ctx fin sis rs m:
   sem_sistate ctx sis rs m ->
-  (forall r, sreg_eval ctx (tr_sis (cf ctx) fin sis) r = Some (tr_regs (cf ctx) fin rs) # r).
+  (forall r, eval_sval ctx (tr_sis (cf ctx) fin sis r) = Some (tr_regs (cf ctx) fin rs) # r).
 Proof.
   Local Opaque str_inputs.
-  unfold sreg_eval; simpl. destruct 1 as (_ & _ & REG).
+  simpl. destruct 1 as (_ & _ & REG).
   destruct fin; simpl; eauto.
 Qed.
 
@@ -842,7 +839,7 @@ Lemma sem_sistate_tr_sis_determ ctx sis rs1 m1 fi rs2 m2:
 Proof.
   intros H1 H2.
   lapply (tr_sis_regs_correct_aux ctx fi sis rs1 m1); eauto.
-  unfold sreg_eval; intros X.
+  intros X.
   destruct H1 as (_&MEM1&REG1).
   destruct H2 as (_&MEM2&REG2); simpl in *.
   intuition try congruence.