From 355671c60fa075b64f64e175bada909a4ce759ac Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 24 Dec 2004 11:25:18 +0000
Subject: Passage d'une bibliothèque de grands entiers naturels vers une
 bibliothèques de grands entiers relatifs munis des 4 opérations de base

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

(limited to 'contrib7')

diff --git a/contrib7/ring/Ring_theory.v b/contrib7/ring/Ring_theory.v
index db3bc55253..a2af9f2607 100644
--- a/contrib7/ring/Ring_theory.v
+++ b/contrib7/ring/Ring_theory.v
@@ -325,8 +325,8 @@ Qed.
 Lemma Th_mult_opp_opp2 : (x,y:A) x*y == (-x)*(-y).
 Symmetry; Apply Th_mult_opp_opp. Qed.
 
-Lemma Th_opp_zero : -0 == 0.
-Rewrite <- (plus_zero_left (-0)).
+Lemma Th_opp_zero : - 0 == 0.
+Rewrite <- (plus_zero_left (- 0)).
 Auto. Qed.
 
 Lemma Th_plus_reg_left : (n,m,p:A) n + m == n + p -> m==p.
-- 
cgit v1.2.3