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 221115bb authored by Sylvain Boulmé's avatar Sylvain Boulmé
Browse files

bug fix ?

parent 91699fd3
......@@ -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:
......
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