diff options
Diffstat (limited to 'scheduling/RTLpathSE_impl.v')
| -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 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: |