From 59e1e2d725febdcae1c9eb478c1f95566ddcc19e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 5 Jun 2007 08:32:28 +0000
Subject: Gestion espaces dans notation _ = _ :> _

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9876 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Notations.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index ffbf83d808..9a0406d591 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -19,13 +19,13 @@ Reserved Notation "~ x" (at level 75, right associativity).
 
 (** Notations for equality and inequalities *)
 
-Reserved Notation "x = y  :> T"
+Reserved Notation "x = y  :>  T"
 (at level 70, y at next level, no associativity).
 Reserved Notation "x = y" (at level 70, no associativity).
 Reserved Notation "x = y = z"
 (at level 70, no associativity, y at next level).
 
-Reserved Notation "x <> y  :> T"
+Reserved Notation "x <> y  :>  T"
 (at level 70, y at next level, no associativity).
 Reserved Notation "x <> y" (at level 70, no associativity).
 
-- 
cgit v1.2.3