Commit 9cddf911 authored by Sylvain Boulmé's avatar Sylvain Boulmé
Browse files

fix comments

parent 75a9af77
......@@ -484,6 +484,11 @@ Definition fScons (hsv: hsval) (lhsv: list_hsval): list_hsval :=
(* TODO: Lemma fScons_correct *)
(* END "fake" hsval ... *)
(** Convert a "fake" hash-consed term into a "real" hash-consed term *)
Fixpoint fsval_proj hsv: ?? hsval :=
match hsv with
| HSinput r hc =>
......@@ -524,8 +529,6 @@ Admitted.
Global Opaque fsval_proj.
Local Hint Resolve fsval_proj_correct: wlp.
(* END "fake" hsval ... *)
(** ** Assignment of memory *)
Definition hslocal_set_smem (hst:hsistate_local) hm :=
{| hsi_smem := hm;
......
Supports Markdown
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