aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/MSets/MSetPositive.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/MSets/MSetPositive.v')
-rw-r--r--theories/MSets/MSetPositive.v5
1 files changed, 0 insertions, 5 deletions
diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v
index e500602fd..369672fab 100644
--- a/theories/MSets/MSetPositive.v
+++ b/theories/MSets/MSetPositive.v
@@ -19,14 +19,9 @@
Require Import Bool BinPos Orders MSetInterface.
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.
-
(** Even if [positive] can be seen as an ordered type with respect to the
usual order (see above), we can also use a lexicographic order over bits