From 98caeb8aa347f5d252b5aafb66f8a7a56942ae15 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date: Fri, 26 Apr 2019 12:24:08 +0200
Subject: [PATCH] Minor clean up

---
 theories/examples/examples.v | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/theories/examples/examples.v b/theories/examples/examples.v
index a36def9..6c500d2 100644
--- a/theories/examples/examples.v
+++ b/theories/examples/examples.v
@@ -7,11 +7,6 @@ From iris.base_logic Require Import invariants.
 
 Section Examples.
   Context `{!heapG Σ} (N : namespace).
-  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,
-     format "⟦  c  @  s  :  sτ  ⟧{ γ }").
 
   Definition seq_example : expr :=
     (let: "c" := new_chan #() in
-- 
GitLab