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

---
 lib/Integers.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'lib/Integers.v')

diff --git a/lib/Integers.v b/lib/Integers.v
index 9c6fcf1d..08a416c1 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -29,6 +29,11 @@ Inductive comparison : Type :=
   | Cgt : comparison               (**r greater than *)
   | Cge : comparison.              (**r greater than or equal *)
 
+Definition comparison_eq: forall (x y: comparison), {x = y} + {x <> y}.
+Proof.
+  decide equality.
+Defined.
+
 Definition negate_comparison (c: comparison): comparison :=
   match c with
   | Ceq => Cne
-- 
cgit