From e858cea149dfffd35ff85fb647b0356564058883 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 31 Jan 2006 10:34:10 +0000
Subject: Ajout décidabilité

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7965 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Bool/Bool.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 0643ba5404..4b41ca746b 100755
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -541,3 +541,10 @@ Proof.
 Qed.
 
 Hint Resolve bool_1 bool_2 bool_3 bool_4 bool_5 bool_6.
+
+(** Decidability *)
+
+Lemma bool_dec : forall a b : bool, {a = b} + { a <> b}.
+Proof.
+  decide equality.
+Defined.
-- 
cgit v1.2.3