aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets/FSetPositive.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/FSets/FSetPositive.v')
-rw-r--r--theories/FSets/FSetPositive.v5
1 files changed, 0 insertions, 5 deletions
diff --git a/theories/FSets/FSetPositive.v b/theories/FSets/FSetPositive.v
index e5d55ac5b..63eab82a5 100644
--- a/theories/FSets/FSetPositive.v
+++ b/theories/FSets/FSetPositive.v
@@ -19,14 +19,9 @@
Require Import Bool BinPos OrderedType OrderedTypeEx FSetInterface.
Set Implicit Arguments.
-
Local Open Scope lazy_bool_scope.
Local Open Scope positive_scope.
-
Local Unset Elimination Schemes.
-Local Unset Case Analysis Schemes.
-Local Unset Boolean Equality Schemes.
-
Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.