From be7661979bc10938f0c9b0e716c080554b34901a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 30 Aug 2016 00:19:34 +0200
Subject: [PATCH] Make namespace type classes opaque.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This way we ensure that Coq gives an error message when one accidentially
writes "N ⊆ E" instead of "nclose N ⊆ E". Before, it used the ⊆ instance of
lists.
---
 program_logic/namespaces.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/program_logic/namespaces.v b/program_logic/namespaces.v
index 02e2a8dd6..5badaaded 100644
--- a/program_logic/namespaces.v
+++ b/program_logic/namespaces.v
@@ -2,6 +2,10 @@ From iris.prelude Require Export countable coPset.
 From iris.algebra Require Export base.
 
 Definition namespace := list positive.
+Instance namespace_dec (N1 N2 : namespace) : Decision (N1 = N2) := _.
+Instance namespace_countable : Countable namespace := _.
+Typeclasses Opaque namespace.
+
 Definition nroot : namespace := nil.
 
 Definition ndot_def `{Countable A} (N : namespace) (x : A) : namespace :=
-- 
GitLab