Implicit Variables Type

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3809 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 6 deletions

diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index 42f44083a..de06c097a 100755
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -14,12 +14,7 @@ Require Lt.
 Require Le.
 Import nat_scope.
 
-Fixpoint minus [n:nat] : nat -> nat := 
-  [m:nat]Cases n m of
-            O    _     =>  O
-         | (S k) O     => (S k)
-         | (S k) (S l) => (minus k l)
-        end. 
+Implicit Variables Type m,n,p:nat.
 
 Lemma minus_plus_simpl : 
 	(n,m,p:nat)((minus n m)=(minus (plus p n) (plus p m))).