aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-07-17 16:10:41 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-07-17 16:10:41 +0000
commit1b701c4f6f6ebf9fc39720fdb3c2990cfc884766 (patch)
tree78a04526973c7d733ea5c91c6cec0c852316109e /theories
parent466c4cbacfb5ffb19ad9a042af7ab1f43441f925 (diff)
"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
Diffstat (limited to 'theories')
-rw-r--r--theories/FSets/FMapPositive.v2
-rw-r--r--theories/FSets/FSetPositive.v5
-rw-r--r--theories/MSets/MSetAVL.v1
-rw-r--r--theories/MSets/MSetGenTree.v1
-rw-r--r--theories/MSets/MSetInterface.v1
-rw-r--r--theories/MSets/MSetPositive.v5
-rw-r--r--theories/MSets/MSetRBT.v1
-rw-r--r--theories/Numbers/BinNums.v2
-rw-r--r--theories/PArith/BinPos.v2
-rw-r--r--theories/PArith/BinPosDef.v2
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.