"Boolean Equality" and "Case Analysis" are already off by default...

 ... no need to Unset them manually

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16631 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 0 insertions, 9 deletions

diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index e719ae441..25d899029 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -38,7 +38,6 @@ Unset Strict Implicit.
 (* for nicer extraction, we create inductive principles
    only when needed *)
 Local Unset Elimination Schemes.
-Local Unset Case Analysis Schemes.
 
 (** * Ops : the pure functions *)
 
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
index b7f3f96c9..3142d97ca 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -34,7 +34,6 @@ Local Open Scope lazy_bool_scope.
 (* For nicer extraction, we create induction principles
    only when needed *)
 Local Unset Elimination Schemes.
-Local Unset Case Analysis Schemes.
 
 Module Type InfoTyp.
  Parameter t : Set.
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index 6778deffa..bd8811689 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -431,7 +431,6 @@ Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E.
 
  (** We avoid creating induction principles for the Record *)
  Local Unset Elimination Schemes.
- Local Unset Case Analysis Schemes.
 
  Definition elt := E.t.
 
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
diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v
index 92ad2fcfb..f0cddcc38 100644
--- a/theories/MSets/MSetRBT.v
+++ b/theories/MSets/MSetRBT.v
@@ -37,7 +37,6 @@ Local Open Scope list_scope.
 (* For nicer extraction, we create induction principles
    only when needed *)
 Local Unset Elimination Schemes.
-Local Unset Case Analysis Schemes.
 
 (** An extra function not (yet?) in MSetInterface.S *)