Merge branch 'nclose_subseteq' into 'master'

Use notation N @⊆ E to avoid ambiguity.

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.

See merge request !24

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