5 files changed, 15 insertions, 0 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 26608a294..aed8c53f5 100755
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -8,6 +8,9 @@
 
 (*i $Id$ i*)
 
+Set Implicit Arguments.
+V7only [Unset Implicit Arguments.].
+
 (** [unit] is a singleton datatype with sole inhabitant [tt] *)
 
 Inductive unit : Set := tt : unit.
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index ab78af469..aace0f804 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -8,6 +8,9 @@
 
 (*i $Id$ i*)
 
+Set Implicit Arguments.
+V7only [Unset Implicit Arguments.].
+
 Require Datatypes.
 
 (** [True] is the always true proposition *)
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index b5a6e6038..5ad3716ed 100755
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -8,6 +8,9 @@
 
 (*i $Id$ i*)
 
+Set Implicit Arguments.
+V7only [Unset Implicit Arguments.].
+
 (** This module defines quantification on the world [Type]
     ([Logic.v] was defining it on the world [Set]) *)
 
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index daf7e5d85..77b9980f9 100755
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -8,6 +8,9 @@
 
 (*i $Id$ i*)
 
+Set Implicit Arguments.
+V7only [Unset Implicit Arguments.].
+
 (** Basic specifications : Sets containing logical information *)
 
 Require Datatypes.
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 4fb640827..01509fa12 100755
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -6,6 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
+Set Implicit Arguments.
+V7only [Unset Implicit Arguments.].
+
 (*i $Id$ i*)
 
 (** This module proves the validity of