From 8d2e6a6617d1cc27121337428c7ec399a26076f7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 26 Nov 2018 16:15:02 +0100
Subject: [PATCH] Add `locC`, the OFE on locations.

---
 theories/heap_lang/lang.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index ad5d655d4..effcebd5f 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -337,6 +337,7 @@ Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
 Instance expr_inhabited : Inhabited expr := populate (Val inhabitant).
 
 Canonical Structure stateC := leibnizC state.
+Canonical Structure locC := leibnizC loc.
 Canonical Structure valC := leibnizC val.
 Canonical Structure exprC := leibnizC expr.
 
-- 
GitLab