From de05e0e6e3869973a5a1dd5427748c3918a6a23d Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Fri, 25 Oct 2019 16:15:04 +0200
Subject: Add 2 missing instances in ZifyBool.v

---
 plugins/micromega/ZifyBool.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'plugins')

diff --git a/plugins/micromega/ZifyBool.v b/plugins/micromega/ZifyBool.v
index 03a7774a31..b94b74097b 100644
--- a/plugins/micromega/ZifyBool.v
+++ b/plugins/micromega/ZifyBool.v
@@ -42,6 +42,16 @@ Instance Op_orb : BinOp orb :=
     TBOpInj := ltac:(destruct n,m; reflexivity)}.
 Add BinOp Op_orb.
 
+Instance Op_implb : BinOp implb :=
+  { TBOp := fun x y => Z.max (1 - x) y;
+    TBOpInj := ltac:(destruct n,m; reflexivity) }.
+Add BinOp Op_implb.
+
+Instance Op_xorb : BinOp xorb :=
+  { TBOp := fun x y => Z.max (x - y) (y - x);
+    TBOpInj := ltac:(destruct n,m; reflexivity) }.
+Add BinOp Op_xorb.
+
 Instance Op_negb : UnOp negb :=
   { TUOp := fun x => 1 - x ; TUOpInj := ltac:(destruct x; reflexivity)}.
 Add UnOp Op_negb.
-- 
cgit v1.2.3