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

2 files changed, 10 insertions, 10 deletions

diff --git a/plugins/ring/Ring_normalize.v b/plugins/ring/Ring_normalize.v
index e499f2220..c6dff3e00 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 41190e8d9..ad75a8a4d 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.