From 35bba4ed67e6872442c6b55084b79c005b8b460b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 14 Jun 2016 16:11:41 +0200
Subject: [PATCH] Some canonical structure instances for heap_lang.

---
 heap_lang/lang.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index 23277892d..62bb4a4c6 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -1,4 +1,5 @@
 From iris.program_logic Require Export ectx_language ectxi_language.
+From iris.algebra Require Export cofe.
 From iris.prelude Require Export strings.
 From iris.prelude Require Import gmap.
 
@@ -508,6 +509,10 @@ Defined.
 
 Instance expr_inhabited X : Inhabited (expr X) := populate (Lit LitUnit).
 Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
+
+Canonical Structure stateC := leibnizC state.
+Canonical Structure valC := leibnizC val.
+Canonical Structure exprC X := leibnizC (expr X).
 End heap_lang.
 
 (** Language *)
-- 
GitLab