1 files changed, 9 insertions, 1 deletions
diff --git a/mppa_k1c/abstractbb/Impure/ImpCore.v b/mppa_k1c/abstractbb/Impure/ImpCore.v
index 6eb0c5af..9745e35c 100644
--- a/mppa_k1c/abstractbb/Impure/ImpCore.v
+++ b/mppa_k1c/abstractbb/Impure/ImpCore.v
@@ -132,6 +132,7 @@ Proof.
   destruct x; simpl; auto.
 Qed.
 
+
 (* Tactics 
 
 MAIN tactics:  
@@ -184,4 +185,11 @@ Ltac wlp_xsimplify hint :=
 
 Create HintDb wlp discriminated.
 
-Ltac wlp_simplify := wlp_xsimplify ltac:(intuition eauto with wlp).
-\ No newline at end of file
+Ltac wlp_simplify := wlp_xsimplify ltac:(intuition eauto with wlp).
+
+(* impure lazy andb of booleans *)
+Definition iandb (k1 k2: ??bool): ?? bool :=
+  DO r1 <~ k1 ;;
+  if r1 then k2 else RET false.
+
+Extraction Inline iandb. (* Juste pour l'efficacité à l'extraction ! *)
+\ No newline at end of file