diff --git a/theories/heap_lang/locations.v b/theories/heap_lang/locations.v
index 53ca9e056f77a5a932435fcfa700aaa6774fe756..3f8e5319661a491f51ba4f5229d5b2b5f48e25dc 100644
--- a/theories/heap_lang/locations.v
+++ b/theories/heap_lang/locations.v
@@ -11,7 +11,7 @@ Instance loc_inhabited : Inhabited loc := populate {|loc_car := 0 |}.
 Instance loc_countable : Countable loc.
 Proof. by apply (inj_countable' loc_car (λ i, {| loc_car := i |})); intros []. Qed.
 
-Program Definition loc_infinite : Infinite loc := {|
+Program Instance loc_infinite : Infinite loc := {|
   infinite_fresh l := {| loc_car := infinite_fresh (loc_car <$> l) |}
 |}.
 Next Obligation.