aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init/Specif.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Init/Specif.v')
-rwxr-xr-xtheories/Init/Specif.v3
1 files changed, 3 insertions, 0 deletions
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.