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
---
 plugins/dp/test2.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/dp')

diff --git a/plugins/dp/test2.v b/plugins/dp/test2.v
index 0940b13524..ce66005207 100644
--- a/plugins/dp/test2.v
+++ b/plugins/dp/test2.v
@@ -73,7 +73,7 @@ zenon.
 Inductive IN (A:Set) : A -> list A -> Prop :=
   | IN1 : forall x l, IN A x (x::l)
   | IN2: forall x l, IN A x l -> forall y, IN A x (y::l).
-Implicit Arguments IN [A].
+Arguments IN [A] _ _.
 
 Goal forall x, forall (l:list nat), IN x l -> IN x (1%nat::l).
   zenon.
-- 
cgit v1.2.3