- notations &&& and ||| equivalent to andb and orb,

  but with lazy behavior while (vm_)computing
- FSetAVL.split has now a dedicated output type instead of ( ,( , ))
- Some proof adaptations.



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

1 files changed, 23 insertions, 2 deletions

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 686118e4b..9db151e32 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -684,7 +684,7 @@ Proof.
   destruct b; intuition.
 Qed.
 
-(* Rewrite rules about andb, orb and if (used in romega) *)
+(** Rewrite rules about andb, orb and if (used in romega) *)
 
 Lemma andb_if : forall (A:Type)(a a':A)(b b' : bool), 
   (if b && b' then a else a') = 
@@ -700,7 +700,28 @@ Proof.
  destruct b; auto.
 Qed.
 
-(* Compatibility *)
+(*****************************************)
+(** * Alternative versions of [andb] and [orb] 
+    with lazy behavior (for vm_compute)  *)
+(*****************************************)
+
+Notation "a &&& b" := (if a then b else false) 
+ (at level 40, left associativity) : bool_scope.
+Notation "a ||| b" := (if a then true else b)
+ (at level 50, left associativity) : bool_scope.
+
+Lemma andb_lazy_alt : forall a b : bool, a && b = a &&& b.
+Proof.
+ unfold andb; auto.
+Qed.
+
+Lemma orb_lazy_alt : forall a b : bool, a || b = a ||| b.
+Proof.
+ unfold orb; auto.
+Qed.
+
+
+(** Compatibility *)
 
 Notation andb := Datatypes.andb (only parsing).
 Notation orb := Datatypes.orb (only parsing).