From 1b3eb3dffae3077d299f1890aa674a3e2ed6d2e2 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date: Thu, 25 Apr 2019 11:28:54 +0200
Subject: [PATCH] Bumped Examples

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

diff --git a/theories/examples.v b/theories/examples.v
index a37b6bc..5787756 100644
--- a/theories/examples.v
+++ b/theories/examples.v
@@ -7,7 +7,7 @@ From iris.base_logic Require Import invariants.
 
 Section Examples.
   Context `{!heapG Σ} (N : namespace).
-  Context `{!logrelG Σ}.
+  Context `{!logrelG val Σ}.
 
   Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st N γ sτ c s)
     (at level 10, s at next level, sτ at next level, γ at next level,
-- 
GitLab