From 884299baa8f87d838ed098aad55179ca42bd0d90 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 30 Aug 2012 16:07:45 +0200
Subject: [PATCH] Change some notations to only parsing.

---
 theories/base.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 06a1a94d..4a193990 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -38,11 +38,11 @@ Notation "(≠ x )" := (λ y, y ≠ x) (only parsing) : C_scope.
 
 Hint Extern 0 (?x = ?x) => reflexivity.
 
-Notation "(→)" := (λ x y, x → y) : C_scope.
-Notation "( T →)" := (λ y, T → y) : C_scope.
-Notation "(→ T )" := (λ y, y → T) : C_scope.
+Notation "(→)" := (λ x y, x → y) (only parsing) : C_scope.
+Notation "( T →)" := (λ y, T → y) (only parsing) : C_scope.
+Notation "(→ T )" := (λ y, y → T) (only parsing) : C_scope.
 Notation "t $ r" := (t r)
-  (at level 65, right associativity,only parsing) : C_scope.
+  (at level 65, right associativity, only parsing) : C_scope.
 Infix "∘" := compose : C_scope.
 Notation "(∘)" := compose (only parsing) : C_scope.
 Notation "( f ∘)" := (compose f) (only parsing) : C_scope.
-- 
GitLab