5 files changed, 15 insertions, 0 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 26608a294d..aed8c53f5e 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 ab78af4699..aace0f804d 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 b5a6e60388..5ad3716ed8 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 daf7e5d85b..77b9980f9c 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 4fb640827b..01509fa121 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