From ed06a90f16fcf7d45672bbddf42efe4cc0efd4d4 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Mon, 21 Nov 2011 17:03:52 +0000
Subject: theories/, plugins/ and test-suite/ ported to the Arguments
 vernacular

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14718 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Natural/Abstract/NDefOps.v    | 2 +-
 theories/Numbers/Natural/Abstract/NStrongRec.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories/Numbers/Natural/Abstract')

diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index 8df715af9d..ad7a9f3ae5 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -23,7 +23,7 @@ Include NStrongRecProp N.
 Definition if_zero (A : Type) (a b : A) (n : N.t) : A :=
   recursion a (fun _ _ => b) n.
 
-Implicit Arguments if_zero [A].
+Arguments if_zero [A] a b n.
 
 Instance if_zero_wd (A : Type) :
  Proper (Logic.eq ==> Logic.eq ==> N.eq ==> Logic.eq) (@if_zero A).
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index 039eefdf59..607746d59e 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -190,7 +190,7 @@ Qed.
 End FixPoint.
 End StrongRecursion.
 
-Implicit Arguments strong_rec [A].
+Arguments strong_rec [A] a f n.
 
 End NStrongRecProp.
 
-- 
cgit v1.2.3