Close an admit

mit-pdos · Dec 17, 2024 · 95f62a5 · 95f62a5
1 parent 2b7c74a
commit 95f62a5
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/src/goose_lang/lifting.v b/src/goose_lang/lifting.v
@@ -197,9 +197,8 @@ Proof.
   rewrite own_globals_unseal.
   rewrite -own_op.
   iApply (own_update_2 with "H1 H2").
-  apply auth_update.
-  (* FIXME: prove local update. *)
-Admitted.
+  by apply auth_update, option_local_update, exclusive_local_update.
+Qed.
 
 Lemma globals_name_init `(hT: globals_preG Σ) (g : gmap string val) :
   ⊢ |==> ∃ new_globals_name : gname, let _ := globalsGS_update_pre Σ hT new_globals_name in