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/Logic/EqdepFacts.v          | 8 ++++----
 theories/Logic/ExtensionalityFacts.v | 4 ++--
 theories/Logic/JMeq.v                | 2 +-
 3 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'theories/Logic')

diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index a341a7a5a9..d84cd82405 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -107,8 +107,8 @@ Section Dependent_Equality.
 
 End Dependent_Equality.
 
-Implicit Arguments eq_dep [U P].
-Implicit Arguments eq_dep1 [U P].
+Arguments eq_dep  [U P] p x q _.
+Arguments eq_dep1 [U P] p x q y.
 
 (** Dependent equality is equivalent to equality on dependent pairs *)
 
@@ -412,5 +412,5 @@ Notation inj_pairT2 := inj_pair2.
 
 End EqdepTheory.
 
-Implicit Arguments eq_dep [].
-Implicit Arguments eq_dep1 [].
+Arguments eq_dep  U P p x q _ : clear implicits.
+Arguments eq_dep1 U P p x q y : clear implicits.
diff --git a/theories/Logic/ExtensionalityFacts.v b/theories/Logic/ExtensionalityFacts.v
index 421bbebcf7..f5e71ef49f 100644
--- a/theories/Logic/ExtensionalityFacts.v
+++ b/theories/Logic/ExtensionalityFacts.v
@@ -42,8 +42,8 @@ Record Delta A := { pi1:A; pi2:A; eq:pi1=pi2 }.
 
 Definition delta {A} (a:A) := {|pi1 := a; pi2 := a; eq := eq_refl a |}.
 
-Implicit Arguments pi1 [[A]].
-Implicit Arguments pi2 [[A]].
+Arguments pi1 {A} _.
+Arguments pi2 {A} _.
 
 Lemma diagonal_projs_same_behavior : forall A (x:Delta A), pi1 x = pi2 x.
 Proof.
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 583d348a2c..753009e682 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -24,7 +24,7 @@ Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop :=
 
 Set Elimination Schemes.
 
-Implicit Arguments JMeq_refl [[A] [x]] [A].
+Arguments JMeq_refl {A x} , [A] x.
 
 Hint Resolve JMeq_refl.
 
-- 
cgit v1.2.3