From cda8d379d0dfcab7e9fb1eab9a861ed1335b8021 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 7 Nov 2003 23:15:28 +0000
Subject: Oubli d'un Set Implicit Arguments

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

diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index 5b3e169684..d5075ffb65 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -18,6 +18,8 @@ Open Local Scope Z_scope.
 (**********************************************************************)
 (* Properties of comparison on Z *)
 
+Set Implicit Arguments.
+
 Theorem Zcompare_Zmult_right : (x,y,z:Z)` z>0` -> `x ?= y`=`x*z ?= y*z`.
 
 Intros; Apply Zcompare_egal_dec;
@@ -139,10 +141,10 @@ Elim (H `|m|`);Intros;Auto with zarith.
 Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial.
 Qed.
 
-(** To do case analysis over the sign of [z] *) 
-
 Unset Implicit Arguments.
 
+(** To do case analysis over the sign of [z] *) 
+
 Lemma Zcase_sign : (x:Z)(P:Prop)
  (`x=0` -> P) ->
  (`x>0` -> P) ->
-- 
cgit v1.2.3