aboutsummaryrefslogtreecommitdiff
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/FSets/FMapList.v2
-rw-r--r--theories/Lists/List.v1
2 files changed, 1 insertions, 2 deletions
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 1b40b09f2a..86f1dfdc20 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -20,8 +20,6 @@ Require Import FMapInterface.
Set Implicit Arguments.
Unset Strict Implicit.
-Arguments Scope list [type_scope].
-
Module Raw (X:OrderedType).
Module E := X.
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 62fc994f99..67b8e43989 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -85,6 +85,7 @@ Delimit Scope list_scope with list.
Bind Scope list_scope with list.
+Arguments Scope list [type_scope].
(** ** Facts about lists *)