From ef95bd7f4afe159bcedc3ec5732579bfc6ba08c6 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Thu, 17 Jun 2021 17:36:42 +0200
Subject: some advance, new section to simplify context from symbolic exec

---
 scheduling/RTLtoBTLproof.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'scheduling/RTLtoBTLproof.v')

diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index 513ed40a..f5c2f3db 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -743,7 +743,7 @@ Theorem transf_program_correct:
 Proof.
   eapply compose_forward_simulations.
   - eapply transf_program_correct_cfg.
-  - eapply cfgsem2fsem.
+  - eapply cfgsem2fsem. eauto.
 Admitted.
 
 End BTL_SIMULATES_RTL.
-- 
cgit