From 8d8ba0ff19430be8708232b219185bf37704756c Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date: Thu, 25 Apr 2019 15:15:52 +0200
Subject: [PATCH] Minor changes

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

diff --git a/theories/examples/proofs_enc.v b/theories/examples/proofs_enc.v
index b0eb0d9..b43ebb6 100644
--- a/theories/examples/proofs_enc.v
+++ b/theories/examples/proofs_enc.v
@@ -7,7 +7,7 @@ From osiris.encodings Require Import stype_enc.
 From osiris.examples Require Import examples.
 
 Section ExampleProofsEnc.
-  Context `{!heapG Σ} {N : namespace}.
+  Context `{!heapG Σ} (N : namespace).
   Context `{!logrelG val Σ}.
 
   Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st N γ (stype'_to_stype sτ) c s)
-- 
GitLab