From 0ee40447f8e35f94b002905a2554c2998f14b7e7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 19 Feb 2017 13:52:23 +0100
Subject: [PATCH] More consistent notations for curried relations.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

For example, instead of:

  Notation "( X ⊆ )"

We now use:

  Notation "( X ⊆)"

We were already doing this for = and ≡.

This solves some conflicts with the notations of MetaCoq.
---
 theories/base.v | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 7b5ae81c..78af51fb 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -642,12 +642,12 @@ Class SubsetEq A := subseteq: relation A.
 Instance: Params (@subseteq) 2.
 Infix "⊆" := subseteq (at level 70) : C_scope.
 Notation "(⊆)" := subseteq (only parsing) : C_scope.
-Notation "( X ⊆ )" := (subseteq X) (only parsing) : C_scope.
-Notation "( ⊆ X )" := (λ Y, Y ⊆ X) (only parsing) : C_scope.
+Notation "( X ⊆)" := (subseteq X) (only parsing) : C_scope.
+Notation "(⊆ X )" := (λ Y, Y ⊆ X) (only parsing) : C_scope.
 Notation "X ⊈ Y" := (¬X ⊆ Y) (at level 70) : C_scope.
 Notation "(⊈)" := (λ X Y, X ⊈ Y) (only parsing) : C_scope.
-Notation "( X ⊈ )" := (λ Y, X ⊈ Y) (only parsing) : C_scope.
-Notation "( ⊈ X )" := (λ Y, Y ⊈ X) (only parsing) : C_scope.
+Notation "( X ⊈)" := (λ Y, X ⊈ Y) (only parsing) : C_scope.
+Notation "(⊈ X )" := (λ Y, Y ⊈ X) (only parsing) : C_scope.
 Infix "⊆*" := (Forall2 (⊆)) (at level 70) : C_scope.
 Notation "(⊆*)" := (Forall2 (⊆)) (only parsing) : C_scope.
 Infix "⊆**" := (Forall2 (⊆*)) (at level 70) : C_scope.
@@ -662,12 +662,12 @@ Hint Extern 0 (_ ⊆** _) => reflexivity.
 
 Infix "⊂" := (strict (⊆)) (at level 70) : C_scope.
 Notation "(⊂)" := (strict (⊆)) (only parsing) : C_scope.
-Notation "( X ⊂ )" := (strict (⊆) X) (only parsing) : C_scope.
-Notation "( ⊂ X )" := (λ Y, Y ⊂ X) (only parsing) : C_scope.
-Notation "X ⊄  Y" := (¬X ⊂ Y) (at level 70) : C_scope.
+Notation "( X ⊂)" := (strict (⊆) X) (only parsing) : C_scope.
+Notation "(⊂ X )" := (λ Y, Y ⊂ X) (only parsing) : C_scope.
+Notation "X ⊄ Y" := (¬X ⊂ Y) (at level 70) : C_scope.
 Notation "(⊄)" := (λ X Y, X ⊄ Y) (only parsing) : C_scope.
-Notation "( X ⊄ )" := (λ Y, X ⊄ Y) (only parsing) : C_scope.
-Notation "( ⊄ X )" := (λ Y, Y ⊄ X) (only parsing) : C_scope.
+Notation "( X ⊄)" := (λ Y, X ⊄ Y) (only parsing) : C_scope.
+Notation "(⊄ X )" := (λ Y, Y ⊄ X) (only parsing) : C_scope.
 
 Notation "X ⊆ Y ⊆ Z" := (X ⊆ Y ∧ Y ⊆ Z) (at level 70, Y at next level) : C_scope.
 Notation "X ⊆ Y ⊂ Z" := (X ⊆ Y ∧ Y ⊂ Z) (at level 70, Y at next level) : C_scope.
-- 
GitLab