From 5ffa8534d09272e5f44c51193e74cffdbc2b043c Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Mon, 7 Oct 2019 15:44:20 +0200
Subject: Icond

---
 mppa_k1c/Op.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'mppa_k1c')

diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index f9a774e8..ce9a5dcd 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -51,6 +51,12 @@ Inductive condition : Type :=
   | Ccompfs (c: comparison)     (**r 32-bit floating-point comparison *)
   | Cnotcompfs (c: comparison). (**r negation of a floating-point comparison *)
 
+Definition condition_eq: forall (x y: condition), {x = y} + {x <> y}.
+Proof.
+  generalize comparison_eq int_eq int64_eq.
+  decide equality.
+Defined.
+
 Inductive condition0 : Type :=
   | Ccomp0 (c: comparison) (**r signed integer comparison with 0 *)
   | Ccompu0 (c: comparison) (**r unsigned integer comparison with 0 *)
-- 
cgit