diff --git a/theories/logatom/elimination_stack/hocap_spec.v b/theories/logatom/elimination_stack/hocap_spec.v
index 9fd1134b1ab284b73b0b53757d400b9731859e65..8db98bffcffbbff9932918380f554b7d4b0740ab 100644
--- a/theories/logatom/elimination_stack/hocap_spec.v
+++ b/theories/logatom/elimination_stack/hocap_spec.v
@@ -27,6 +27,8 @@ Record hocap_stack {Σ} `{!heapG Σ} := AtomicStack {
   pop : val;
   (* -- other data -- *)
   name : Type;
+  name_eqdec : EqDecision name;
+  name_countable : Countable name;
   (* -- predicates -- *)
   is_stack (N : namespace) (γs : name) (v : val) : iProp Σ;
   stack_content_frag (γs : name) (l : list val) : iProp Σ;
@@ -61,9 +63,9 @@ Record hocap_stack {Σ} `{!heapG Σ} := AtomicStack {
 }.
 Arguments hocap_stack _ {_}.
 
-Existing Instance is_stack_persistent.
-Existing Instance stack_content_frag_timeless.
-Existing Instance stack_content_auth_timeless.
+Existing Instances
+  is_stack_persistent stack_content_frag_timeless stack_content_auth_timeless
+  name_eqdec name_countable.
 
 (** Show that our way of writing the [pop_spec] is equivalent to what is done in
 [concurrent_stack.spec].  IOW, the conjunction-vs-match doesn't matter.  Fixing
diff --git a/theories/logatom/elimination_stack/spec.v b/theories/logatom/elimination_stack/spec.v
index 7cd3c880d9bba034052b3ed7ab48922f8cfd3208..b00472e49f193b20d4d84a9cbcdca468c1e7bb56 100644
--- a/theories/logatom/elimination_stack/spec.v
+++ b/theories/logatom/elimination_stack/spec.v
@@ -11,6 +11,8 @@ Record atomic_stack {Σ} `{!heapG Σ} := AtomicStack {
   pop : val;
   (* -- other data -- *)
   name : Type;
+  name_eqdec : EqDecision name;
+  name_countable : Countable name;
   (* -- predicates -- *)
   is_stack (N : namespace) (γs : name) (v : val) : iProp Σ;
   stack_content (γs : name) (l : list val) : iProp Σ;
@@ -36,5 +38,6 @@ Record atomic_stack {Σ} `{!heapG Σ} := AtomicStack {
 }.
 Arguments atomic_stack _ {_}.
 
-Existing Instance is_stack_persistent.
-Existing Instance stack_content_timeless.
+Existing Instances
+  is_stack_persistent stack_content_timeless
+  name_countable name_eqdec.
diff --git a/theories/logatom/snapshot/spec.v b/theories/logatom/snapshot/spec.v
index c9b00ef9fd6dc1694c9a0ae658abc347840073a4..1866b8ab62bfcd0752d6b875c96ed722b2d0d243 100644
--- a/theories/logatom/snapshot/spec.v
+++ b/theories/logatom/snapshot/spec.v
@@ -17,6 +17,8 @@ Record atomic_snapshot {Σ} `{!heapG Σ} := AtomicSnapshot {
     readPair : val;
     (* other data *)
     name: Type;
+    name_eqdec : EqDecision name;
+    name_countable : Countable name;
     (* predicates *)
     is_pair (N : namespace) (γ : name) (p : val) : iProp Σ;
     pair_content (γ : name) (a: val * val) : iProp Σ;
@@ -48,3 +50,7 @@ Record atomic_snapshot {Σ} `{!heapG Σ} := AtomicSnapshot {
       <<< pair_content γ (v1, v2), RET (v1, v2) >>>;
 }.
 Arguments atomic_snapshot _ {_}.
+
+Existing Instances
+  is_pair_persistent pair_content_timeless
+  name_countable name_eqdec.