From 412c877f20ffceb407f2622bdfe6557a3df4062a Mon Sep 17 00:00:00 2001
From: pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sun, 12 Dec 2010 14:04:00 +0000
Subject: Sorry for the mistake in r13702

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

(limited to 'theories/Arith')

diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index eb2d4df4c..02975d8f1 100644
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -1,4 +1,4 @@
-(************************************************************************)
+ (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
@@ -26,7 +26,7 @@ Implicit Types m n p q : nat.
 
 (** * Zero is neutral 
 Deprecated : Already in Init/Peano.v *)
-Definition plus_0_l n := eq_sym (plus_O_n n).
+Notation plus_0_l := plus_O_n (only parsing).
 Definition plus_0_r n := eq_sym (plus_n_O n).
 
 (** * Commutativity *)
-- 
cgit v1.2.3