From ef486799ac73c533e0a5b5cdd2662eb68a2636cb Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 28 Apr 2007 10:30:25 +0000
Subject: Déplacement des opérations sur bool dans l'état initial
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9803 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Bool/Bool.v | 26 +-------------------------
 1 file changed, 1 insertion(+), 25 deletions(-)

(limited to 'theories/Bool')

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          *)
 (****************************)
-- 
cgit v1.2.3