Ajout operation eq dans PMap et IndexedMap

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@158 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 10 insertions, 0 deletions

diff --git a/lib/Maps.v b/lib/Maps.v
index 69690918..22d9a370 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -801,6 +801,14 @@ Module PMap <: MAP.
 
   Definition t (A : Set) : Set := (A * PTree.t A)%type.
 
+  Definition eq: forall (A: Set), (forall (x y: A), {x=y} + {x<>y}) ->
+                 forall (a b: t A), {a = b} + {a <> b}.
+  Proof.
+    intros. 
+    generalize (PTree.eq H). intros. 
+    decide equality.
+  Qed.
+
   Definition init (A : Set) (x : A) :=
     (x, PTree.empty A).
 
@@ -877,6 +885,8 @@ Module IMap(X: INDEXED_TYPE).
   Definition elt := X.t.
   Definition elt_eq := X.eq.
   Definition t : Set -> Set := PMap.t.
+  Definition eq: forall (A: Set), (forall (x y: A), {x=y} + {x<>y}) ->
+                 forall (a b: t A), {a = b} + {a <> b} := PMap.eq.
   Definition init (A: Set) (x: A) := PMap.init x.
   Definition get (A: Set) (i: X.t) (m: t A) := PMap.get (X.index i) m.
   Definition set (A: Set) (i: X.t) (v: A) (m: t A) := PMap.set (X.index i) v m.