From 95b6814a1cff386150a7573cb30e9cb68a18052c Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Mon, 10 May 2021 20:07:29 +0200
Subject: prove sexec_exact

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

(limited to 'scheduling/BTL.v')

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index a87f674b..476e71a7 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -153,7 +153,7 @@ Inductive state : Type :=
       state.
 
 (** outcome of a block execution *)
-Record outcome := {
+Record outcome := out {
    _rs: regset;
    _m: mem;
    _fin: option final 
-- 
cgit