From 2311cb788e6dcf0103266fd6c6aa76096c283e34 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Fri, 28 May 2021 16:33:23 +0200
Subject: remove dupmap from BTL_Scheduler !

---
 scheduling/BTL_Schedulerproof.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'scheduling/BTL_Schedulerproof.v')

diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v
index 049dc6b1..c8c2a76f 100644
--- a/scheduling/BTL_Schedulerproof.v
+++ b/scheduling/BTL_Schedulerproof.v
@@ -24,6 +24,8 @@ Let tpge := Genv.globalenv tprog.
 
 Theorem transf_program_correct:
   forward_simulation (fsem prog) (fsem tprog).
+Proof.
+  eapply forward_simulation_step with equiv_state. (* lock-step with respect to equiv_states *)
 Admitted.
 
 End PRESERVATION.
-- 
cgit