Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit 9a0cf394 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-work

parents a3d782f1 221115bb
......@@ -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:
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment