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/ring/Ring_normalize.v        | 10 +++++-----
 plugins/ring/Setoid_ring_normalize.v | 10 +++++-----
 2 files changed, 10 insertions(+), 10 deletions(-)

(limited to 'plugins/ring')

diff --git a/plugins/ring/Ring_normalize.v b/plugins/ring/Ring_normalize.v
index e499f22201..c6dff3e006 100644
--- a/plugins/ring/Ring_normalize.v
+++ b/plugins/ring/Ring_normalize.v
@@ -746,11 +746,11 @@ Qed.
 (* End properties. *)
 End semi_rings.
 
-Implicit Arguments Cons_varlist.
-Implicit Arguments Cons_monom.
-Implicit Arguments SPconst.
-Implicit Arguments SPplus.
-Implicit Arguments SPmult.
+Arguments Cons_varlist : default implicits.
+Arguments Cons_monom : default implicits.
+Arguments SPconst : default implicits.
+Arguments SPplus : default implicits.
+Arguments SPmult : default implicits.
 
 Section rings.
 
diff --git a/plugins/ring/Setoid_ring_normalize.v b/plugins/ring/Setoid_ring_normalize.v
index 41190e8d9a..ad75a8a4dd 100644
--- a/plugins/ring/Setoid_ring_normalize.v
+++ b/plugins/ring/Setoid_ring_normalize.v
@@ -1011,11 +1011,11 @@ Qed.
 
 End semi_setoid_rings.
 
-Implicit Arguments Cons_varlist.
-Implicit Arguments Cons_monom.
-Implicit Arguments SetSPconst.
-Implicit Arguments SetSPplus.
-Implicit Arguments SetSPmult.
+Arguments Cons_varlist : default implicits.
+Arguments Cons_monom : default implicits.
+Arguments SetSPconst : default implicits.
+Arguments SetSPplus : default implicits.
+Arguments SetSPmult : default implicits.
 
 
 
-- 
cgit v1.2.3