"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

10 files changed, 0 insertions, 22 deletions

diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 5e968d4d3..792b88717 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -12,9 +12,7 @@ Require Import Bool ZArith OrderedType OrderedTypeEx FMapInterface.
 
 Set Implicit Arguments.
 Local Open Scope positive_scope.
-
 Local Unset Elimination Schemes.
-Local Unset Case Analysis Schemes.
 
 (** This file is an adaptation to the [FMap] framework of a work by
   Xavier Leroy and Sandrine Blazy (used for building certified compilers).
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.
 
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 *)
 
diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v
index aab2c14fa..6a521d6b6 100644
--- a/theories/Numbers/BinNums.v
+++ b/theories/Numbers/BinNums.v
@@ -9,8 +9,6 @@
 (** * Binary Numerical Datatypes *)
 
 Set Implicit Arguments.
-(* For compatibility, we will not use generic equality functions *)
-Local Unset Boolean Equality Schemes.
 
 Declare ML Module "z_syntax_plugin".
 
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index aa065e3c5..7f478546e 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -23,8 +23,6 @@ Require Export BinPosDef.
     are now defined in [BinNums.v] *)
 
 Local Open Scope positive_scope.
-Local Unset Boolean Equality Schemes.
-Local Unset Case Analysis Schemes.
 
 (** Every definitions and early properties about positive numbers
     are placed in a module [Pos] for qualification purpose. *)
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index 6d85f0723..61bee69f8 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -30,8 +30,6 @@ Notation "p ~ 0" := (xO p)
  (at level 7, left associativity, format "p '~' '0'") : positive_scope.
 
 Local Open Scope positive_scope.
-Local Unset Boolean Equality Schemes.
-Local Unset Case Analysis Schemes.
 
 Module Pos.