diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-01 13:17:45 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-01 13:17:45 +0100 |
| commit | 9a0cf394fb3b3e0e7ae064c4d7cec218c52a2828 (patch) | |
| tree | 60e0d5c1ded917966f7c25b67c8bdf11ebd3632e /scheduling/RTLpathSE_impl.v | |
| parent | a3d782f1d30bfea3fee4ac60c6a5aa36c2f5de25 (diff) | |
| parent | 221115bbc18cdb40c8d2e571940b48ec7e80029a (diff) | |
| download | compcert-kvx-9a0cf394fb3b3e0e7ae064c4d7cec218c52a2828.tar.gz compcert-kvx-9a0cf394fb3b3e0e7ae064c4d7cec218c52a2828.zip | |
Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-work
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 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: |