minor cleanup

theories/typing/lib/ghostcell.v

@@ -443,7 +443,7 @@ Section ghostcell.
   Definition ghostset_new (call_once : val) (R_F : type) : val :=
     funrec: <> ["f"] :=
       let: "call_once" := call_once in
-      let: "n" := new (#0::nil) in
+      let: "n" := new [ #0] in
       letcall: "r" := "call_once" ["f";"n"]%E in
       letalloc: "r'" <-{ R_F.(ty_size)} !"r" in
       delete [ #R_F.(ty_size); "r"];;
@@ -504,7 +504,7 @@ Section ghostcell.
       return: ["n"].
 
   Lemma ghostcell_new_type `{!TyWf ty} :
-    typed_val ghostcell_new (fn(∀ '(α), ∅; ty) → (ghostcell α ty))%T.
+    typed_val ghostcell_new (fn(∀ α, ∅; ty) → (ghostcell α ty))%T.
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
     iIntros (α ϝ ϝl qϝl ret args). inv_vec args=>n. simpl_subst.
@@ -733,7 +733,8 @@ Section ghostcell.
   (* Don't reevaluate *)
    Definition ghostcell_get_mut : val :=
     funrec: <> ["s";"c"] :=
-      Endlft ;;
+      Skip ;;
+      Skip ;;
       Skip ;;
       return: ["c"].