Déplacement des opérations sur bool dans l'état initial

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

1 files changed, 1 insertions, 25 deletions

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index d8b900686..1bd56a1ee 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -126,9 +126,8 @@ Proof.
   destruct a; destruct b; simpl in |- *; intro; discriminate H || reflexivity.
 Qed.
 
-
 (************************)
-(** * Logical combinators *)
+(** * A synonym of [if] on [bool] *)
 (************************)
  
 Definition ifb (b1 b2 b3:bool) : bool :=
@@ -137,31 +136,8 @@ Definition ifb (b1 b2 b3:bool) : bool :=
     | false => b3
   end.
 
-Definition andb (b1 b2:bool) : bool := ifb b1 b2 false.
-
-Definition orb (b1 b2:bool) : bool := ifb b1 true b2.
-
-Definition implb (b1 b2:bool) : bool := ifb b1 b2 true.
-
-Definition xorb (b1 b2:bool) : bool :=
-  match b1, b2 with
-    | true, true => false
-    | true, false => true
-    | false, true => true
-    | false, false => false
-  end.
-
-Definition negb (b:bool) := if b then false else true.
-
-Infix "||" := orb (at level 50, left associativity) : bool_scope.
-Infix "&&" := andb (at level 40, left associativity) : bool_scope.
-
 Open Scope bool_scope.
 
-Delimit Scope bool_scope with bool.
-
-Bind Scope bool_scope with bool.
-
 (****************************)
 (** * De Morgan laws          *)
 (****************************)