From 561dcedd6bb9bf037d60a64385433c13bf9196a0 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 1 Dec 2003 12:31:32 +0000
Subject: Meilleure robustesse des reordonnement d'arguments (2eme)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5049 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories7/Arith/Plus.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories7/Arith/Plus.v b/theories7/Arith/Plus.v
index efd8ce83aa..f6ea71de74 100755
--- a/theories7/Arith/Plus.v
+++ b/theories7/Arith/Plus.v
@@ -68,7 +68,7 @@ Hints Resolve plus_assoc_r : arith v62.
 
 (** Simplification *)
 
-Lemma plus_reg_l : (n,m,p:nat)((p+n)=(p+m))->(n=m).
+Lemma plus_reg_l : (m,p,n:nat)((n+m)=(n+p))->(m=p).
 Proof.
 Intros m p n; NewInduction n ; Simpl ; Auto with arith.
 Qed.
-- 
cgit v1.2.3