From 8752cea89f862d92d49183fe10d1918588143ab1 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 28 May 2021 12:38:05 +0200 Subject: fix some merge errors --- scheduling/BTL_SEtheory.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'scheduling/BTL_SEtheory.v') diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index cea69f55..5b15fe9b 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -731,7 +731,7 @@ pour représenter l'ensemble des chemins. Fixpoint sexec_rec f ib sis (k: sistate -> sstate): sstate := match ib with - | BF fin => Sfinal (tr_sis f fin sis) (sexec_final_sfv fin sis) + | BF fin _ => Sfinal (tr_sis f fin sis) (sexec_final_sfv fin sis) (* basic instructions *) | Bnop _ => k sis | Bop op args res _ => k (sexec_op op args res sis) -- cgit