From ff41fb77e754d19c7a65ed8006e3b5ef5c3fd064 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Sun, 10 Apr 2022 01:35:21 +0200
Subject: [PATCH] Made heapGS_step_cnt a local instance
---
iris_heap_lang/primitive_laws.v | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index ae9d3dade..e51974e02 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -17,8 +17,9 @@ Class heapGS Σ := HeapGS {
heapGS_inv_heapGS :> inv_heapGS loc (option val) Σ;
heapGS_proph_mapGS :> proph_mapGS proph_id (val * val) Σ;
heapGS_step_name : gname;
- heapGS_step_cnt :> mono_natG Σ;
+ heapGS_step_cnt : mono_natG Σ;
}.
+Local Existing Instance heapGS_step_cnt.
Section steps.
Context `{!heapGS Σ}.
--
GitLab