Uniformisation (Qed/Save et Implicits Arguments)

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

9 files changed, 18 insertions, 18 deletions

diff --git a/contrib/correctness/ArrayPermut.v b/contrib/correctness/ArrayPermut.v
index d183df49c7..55259b943d 100644
--- a/contrib/correctness/ArrayPermut.v
+++ b/contrib/correctness/ArrayPermut.v
@@ -21,7 +21,7 @@ Require Export Exchange.
 
 Require Omega.
 
-Implicit Arguments On.
+Set Implicit Arguments.
 
 (* We define "permut" as the smallest equivalence relation which contains
  * transpositions i.e. exchange of two elements.
diff --git a/contrib/correctness/Arrays.v b/contrib/correctness/Arrays.v
index 10ba81719c..acf26ed3d5 100644
--- a/contrib/correctness/Arrays.v
+++ b/contrib/correctness/Arrays.v
@@ -29,7 +29,7 @@
 
 Require Export ProgInt.
 
-Implicit Arguments On.
+Set Implicit Arguments.
 
 
 (* The type of arrays *)
diff --git a/contrib/correctness/Exchange.v b/contrib/correctness/Exchange.v
index ddad80b35f..85c19b48bc 100644
--- a/contrib/correctness/Exchange.v
+++ b/contrib/correctness/Exchange.v
@@ -18,7 +18,7 @@
 Require ProgInt.
 Require Arrays.
 
-Implicit Arguments On.
+Set Implicit Arguments.
 
 (* Definition *)
 
diff --git a/contrib/correctness/Sorted.v b/contrib/correctness/Sorted.v
index 287d1dbeb8..9dc9d066ab 100644
--- a/contrib/correctness/Sorted.v
+++ b/contrib/correctness/Sorted.v
@@ -16,7 +16,7 @@ Require ArrayPermut.
 Require ZArithRing.
 Require Omega.
 
-Implicit Arguments On.
+Set Implicit Arguments.
 
 (* Definition *)
 
diff --git a/contrib/ring/Quote.v b/contrib/ring/Quote.v
index f97c81c408..1565e522b4 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 ae72f4eb4c..564a540982 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 1b787f4239..34bc697d49 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 8b889b23f2..ec5f32fc2f 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 0192dce9e2..15f79158f3 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.