Uniformisation (Qed/Save et Implicits Arguments)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2651 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 14 insertions, 14 deletions

diff --git a/contrib/ring/Quote.v b/contrib/ring/Quote.v
index f97c81c40..1565e522b 100644
--- a/contrib/ring/Quote.v
+++ b/contrib/ring/Quote.v
@@ -25,7 +25,7 @@
 
 ***********************************************************************)
 
-Implicit Arguments On.
+Set Implicit Arguments.
 
 Section variables_map.
 
@@ -82,7 +82,7 @@ Save.
 
 End variables_map.
 
-Implicit Arguments Off.
+Unset Implicit Arguments.
 
 Declare ML Module "quote".
 
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v
index ae72f4eb4..564a54098 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/contrib/ring/Ring_normalize.v
@@ -11,7 +11,7 @@
 Require Ring_theory.
 Require Quote.
 
-Implicit Arguments On.
+Set Implicit Arguments.
 
 Lemma index_eq_prop: (n,m:index)(Is_true (index_eq n m)) -> n=m.
 Proof.
@@ -332,7 +332,7 @@ Fixpoint interp_sp [p:spolynomial] : A :=
 
 (* End interpretation. *)
 
-Implicit Arguments Off.
+Unset Implicit Arguments.
 
 (* Section properties. *)
 
@@ -758,7 +758,7 @@ Section rings.
 
 (* Here the coercion between Ring and Semi-Ring will be useful *)
 
-Implicit Arguments On.
+Set Implicit Arguments.
 
 Variable A : Type.
 Variable Aplus : A -> A -> A.
@@ -849,7 +849,7 @@ Fixpoint interp_p [p:polynomial] : A :=
 
 (*** Properties *)
 
-Implicit Arguments Off.
+Unset Implicit Arguments.
 
 Lemma spolynomial_of_ok : (p:polynomial)
   (interp_p p)==(interp_sp Aplus Amult Azero vm (spolynomial_of p)).
diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v
index 1b787f423..34bc697d4 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/Ring_theory.v
@@ -10,7 +10,7 @@
 
 Require Export Bool.
 
-Implicit Arguments On.
+Set Implicit Arguments.
 
 Grammar ring formula : constr :=
   formula_expr [ expr($p) ] -> [$p]
@@ -379,7 +379,7 @@ End Theory_of_rings.
 
 Hints Resolve Th_mult_zero_left Th_plus_reg_left : core.
 
-Implicit Arguments Off.
+Unset Implicit Arguments.
 
 Definition Semi_Ring_Theory_of :
   (A:Type)(Aplus : A -> A -> A)(Amult : A -> A -> A)(Aone : A)
diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v
index 8b889b23f..ec5f32fc2 100644
--- a/contrib/ring/Setoid_ring_normalize.v
+++ b/contrib/ring/Setoid_ring_normalize.v
@@ -11,7 +11,7 @@
 Require Setoid_ring_theory.
 Require Quote.
 
-Implicit Arguments On.
+Set Implicit Arguments.
 
 Lemma index_eq_prop: (n,m:index)(Is_true (index_eq n m)) -> n=m.
 Proof.
@@ -348,7 +348,7 @@ Fixpoint interp_setsp [p:setspolynomial] : A :=
 
 (* End interpretation. *)
 
-Implicit Arguments Off.
+Unset Implicit Arguments.
 
 (* Section properties. *)
 
@@ -1014,7 +1014,7 @@ Implicits SetSPmult.
 
 Section setoid_rings.
 
-Implicit Arguments On.
+Set Implicit Arguments.
 
 Variable vm : (varmap A).
 Variable T : (Setoid_Ring_Theory A Aequiv Aplus Amult Aone Azero Aopp Aeq).
@@ -1098,7 +1098,7 @@ Fixpoint interp_setp [p:setpolynomial] : A :=
 
 (*** Properties *)
 
-Implicit Arguments Off.
+Unset Implicit Arguments.
 
 Lemma setspolynomial_of_ok : (p:setpolynomial)
  (Aequiv (interp_setp p) (interp_setsp vm (setspolynomial_of p))).
diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v
index 0192dce9e..15f79158f 100644
--- a/contrib/ring/Setoid_ring_theory.v
+++ b/contrib/ring/Setoid_ring_theory.v
@@ -11,7 +11,7 @@
 Require Export Bool.
 Require Export Setoid.
 
-Implicit Arguments On.
+Set Implicit Arguments.
 
 Grammar ring formula : constr :=
   formula_expr [ expr($p) ] -> [$p]
@@ -430,7 +430,7 @@ End Theory_of_setoid_rings.
 
 Hints Resolve STh_mult_zero_left STh_plus_reg_left : core.
 
-Implicit Arguments Off.
+Unset Implicit Arguments.
 
 Definition Semi_Setoid_Ring_Theory_of :
   Setoid_Ring_Theory -> Semi_Setoid_Ring_Theory.