From e9a19f543edc02740093ec334d974f9021052a3d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 1 Jun 2019 15:38:29 +0200
Subject: [PATCH] forgot to make it an Instance

---
 theories/heap_lang/locations.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/heap_lang/locations.v b/theories/heap_lang/locations.v
index 53ca9e056..3f8e53196 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.
-- 
GitLab