diff --git a/theories/examples/proofs_enc.v b/theories/examples/proofs_enc.v
index b0eb0d9f2ccad09a1170d48c86474915bd0442ef..b43ebb6deb7b6916e56bb9349d96fb1c105ddee9 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)