Now actually did that.

7005ba64 · Ike Mulder · 5d0722f1 · 7005ba64
Commit 7005ba64 authored Mar 30, 2022 by Ike Mulder
--- a/theories/examples/wip/logatom/atomic_clhlock.v
+++ b/theories/examples/wip/logatom/atomic_clhlock.v
@@ -123,7 +123,7 @@ Section spec.
      new_node #() 
    {{ (n : loc), RET #n; free_node n }}.

-  Global Instance new_lock_spec :
+  Global Program Instance new_lock_spec :
    SPEC {{ True }} 
      new_lock #() 
    {{ (l p : loc) γe, RET #l; holds_at_loc l (is_queued_loc γe) ∗ is_queue_head γe p }}.