From 615fb53c13f2407a0b6b470bbdf8e468fc4a1d78 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 5 Jun 2009 13:39:59 +0000
Subject: Adapted to work with Coq 8.2-1

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1076 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 lib/Ordered.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

(limited to 'lib/Ordered.v')

diff --git a/lib/Ordered.v b/lib/Ordered.v
index 4b1f4e0f..eddc3721 100644
--- a/lib/Ordered.v
+++ b/lib/Ordered.v
@@ -45,6 +45,8 @@ Proof.
   assert (Zpos x <> Zpos y). congruence. omega.
 Qed.
 
+Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := peq.
+
 End OrderedPositive.
 
 (** Indexed types (those that inject into [positive]) are ordered. *)
@@ -81,6 +83,13 @@ Proof.
   apply GT. exact l.
 Qed.
 
+Lemma eq_dec : forall x y, { eq x y } + { ~ eq x y }.
+Proof.
+  intros. case (peq (A.index x) (A.index y)); intros.
+  left. apply A.index_inj; auto.
+  right; red; unfold eq; intros; subst. congruence. 
+Qed.
+
 End OrderedIndexed.
 
 (** The product of two ordered types is ordered. *)
@@ -164,5 +173,15 @@ Proof.
   apply GT. red. left. auto.
 Qed.
 
+Lemma eq_dec : forall x y, { eq x y } + { ~ eq x y }.
+Proof.
+  unfold eq; intros.
+  case (A.eq_dec (fst x) (fst y)); intros.
+  case (B.eq_dec (snd x) (snd y)); intros.
+  left; auto.
+  right; intuition.
+  right; intuition.
+Qed.
+
 End OrderedPair.
 
-- 
cgit