diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-03-01 13:12:58 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-03-01 13:12:58 +0100 |
| commit | 221115bbc18cdb40c8d2e571940b48ec7e80029a (patch) | |
| tree | e3a3fb24b31518f0cd434fc3da8ca581a3d0637b | |
| parent | 91699fd379eb4087eb4088af77a5eb918552dc5e (diff) | |
| download | compcert-kvx-221115bbc18cdb40c8d2e571940b48ec7e80029a.tar.gz compcert-kvx-221115bbc18cdb40c8d2e571940b48ec7e80029a.zip | |
bug fix ?
| -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: |