diff options
| -rw-r--r-- | scheduling/RTLpathSE_impl.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index 06fdaab4..f98dc11c 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -449,13 +449,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 @@ -463,7 +463,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: |