From 9f252d9055ad16f9433caaf41f6490e45424e88a Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Wed, 19 May 2021 15:53:02 +0200
Subject: Adding a BTL record to help oracles

---
 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 f89ea5cf..6681d691 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -215,7 +215,7 @@ type defined below. Intuitively, each RTL step corresponds to either
 Fixpoint measure ib: nat :=
   match ib with
   | Bseq ib1 ib2
-  | Bcond _ _ ib1 ib2 _ => measure ib1 + measure ib2
+  | Bcond _ _ ib1 ib2 _ _ => measure ib1 + measure ib2
   | ib => 1
   end.
 
-- 
cgit