Uniformisation (Qed/Save et Implicits Arguments)

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

4 files changed, 4 insertions, 4 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 *)