From b0452edc5e911d8585a691ad4e530d4f1427f463 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Mon, 22 Feb 2021 16:09:53 +0100 Subject: a bit more cleaning --- scheduling/RTLpathSE_impl.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'scheduling/RTLpathSE_impl.v') diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index bd26171d..bdd4bda8 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -764,7 +764,7 @@ Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) : DO vargs <~ hlist_args prev args ;; let ex := {| hsi_cond:=cond; hsi_scondargs:=vargs; hsi_elocal := prev; hsi_ifso := ifso |} in RET (Some {| hsi_pc := ifnot; hsi_exits := ex::hst.(hsi_exits); hsi_local := prev |}) - | _ => RET None (* TODO jumptable ? *) + | _ => RET None end. -- cgit