From bf6caa7f7443d46b2046b4fb6cd8164c69f9a9cd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 18 Nov 2016 11:56:55 +0100
Subject: [PATCH] Make nclose an explicit coercion.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

We do this by introducing a type class UpClose with notation ↑.

The reason for this change is as follows: since `nclose : namespace
→ coPset` is declared as a coercion, the notation `nclose N ⊆ E` was
pretty printed as `N ⊆ E`. However, `N ⊆ E` could not be typechecked
because type checking goes from left to right, and as such would look
for an instance `SubsetEq namespace`, which causes the right hand side
to be ill-typed.
---
 theories/base.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/base.v b/theories/base.v
index 4284a896..51dcdad2 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -726,6 +726,8 @@ End disjoint_list.
 
 Class Filter A B := filter: ∀ (P : A → Prop) `{∀ x, Decision (P x)}, B → B.
 
+Class UpClose A B := up_close : A → B.
+Notation "↑ x" := (up_close x) (at level 20, format "↑ x").
 
 (** * Monadic operations *)
 (** We define operational type classes for the monadic operations bind, join 
-- 
GitLab