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/Cyclic/Abstract/CyclicAxioms.v   | 2 +-
 theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories/Numbers/Cyclic')

diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 3aa0753840..59656eedbe 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -204,7 +204,7 @@ Module ZnZ.
 
  End Specs.
 
- Implicit Arguments Specs [[t]].
+ Arguments Specs {t} ops.
 
  (** Generic construction of double words *)
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
index 073afec37b..a274b8395b 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
@@ -53,7 +53,7 @@ Section Zn2Z.
 
 End Zn2Z.
 
-Implicit Arguments W0 [znz].
+Arguments W0 [znz].
 
 (** From a cyclic representation [w], we iterate the [zn2z] construct
     [n] times, gaining the type of binary trees of depth at most [n],
-- 
cgit v1.2.3