diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-07 23:15:28 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-07 23:15:28 +0000 |
| commit | cda8d379d0dfcab7e9fb1eab9a861ed1335b8021 (patch) | |
| tree | 485d89fa4bd0e3de41d58c6f65a6a543c6d7a3e7 /theories/ZArith/Zcomplements.v | |
| parent | fb07608cdd6c530cf8360f4f8fe0a0d34729ad43 (diff) | |
Oubli d'un Set Implicit Arguments
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4825 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Zcomplements.v')
| -rw-r--r-- | theories/ZArith/Zcomplements.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index 5b3e16968..d5075ffb6 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) -> |