From 221115bbc18cdb40c8d2e571940b48ec7e80029a Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Mon, 1 Mar 2021 13:12:58 +0100 Subject: bug fix ? --- scheduling/RTLpathSE_impl.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'scheduling/RTLpathSE_impl.v') diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index d4ea09d6..1ae5c773 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -505,13 +505,13 @@ Fixpoint fsval_proj hsv: ?? hsval := else RET hsv (* already hash-consed *) | HSload hm t chk addr hl _ => RET hsv (* FIXME ? *) end -with fsval_list_proj hl: ?? list_hsval := - match hl with +with fsval_list_proj hsl: ?? list_hsval := + match hsl with | HSnil hc => DO b <~ phys_eq hc unknown_hid;; if b then hSnil() (* was not yet really hash-consed *) - else RET hl (* already hash-consed *) + else RET hsl (* already hash-consed *) | HScons hv hl hc => DO b <~ phys_eq hc unknown_hid;; if b @@ -519,7 +519,7 @@ with fsval_list_proj hl: ?? list_hsval := DO hv' <~ fsval_proj hv;; DO hl' <~ fsval_list_proj hl;; hScons hv' hl' - else RET hl (* already hash-consed *) + else RET hsl (* already hash-consed *) end. Lemma fsval_proj_correct hsv: -- cgit