From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 8 Sep 2005 10:36:40 +0000 (+0000)
Subject: uses Map.equal to compare universes
X-Git-Tag: V_0_1_2_1~62
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=533cbf996d38fabd40195e2184191d350b831ad2;p=helm.git

uses Map.equal to compare universes
---

diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml
index e79a2a9d9..5616cb675 100644
--- a/helm/ocaml/cic/cicUniv.ml
+++ b/helm/ocaml/cic/cicUniv.ml
@@ -98,28 +98,7 @@ let are_entry_eq v1 v2 =
   (are_set_eq v1.one_s_gt v2.one_s_gt ) &&
   (are_set_eq v1.one_s_eq v2.one_s_eq )
 
-
-(* ocaml 3.07 doesn't have MAP.equal, 3.08 has it! *)
-(*
-  let are_ugraph_eq308 g h =
-    MAL.equal are_entry_eq g h
-*)
-let are_ugraph_eq307 g h = 
-  try
-    MAL.fold (
-      fun k v b -> 
-        if not b then 
-          raise (Failure "Different") 
-        else
-          try
-            let k_h = MAL.find k h in
-            are_entry_eq v k_h
-          with Not_found -> true
-        ) g true
-    with 
-      Failure "Different" -> false
-
-let are_ugraph_eq = are_ugraph_eq307
+let are_ugraph_eq = MAL.equal are_entry_eq
 
 (*****************************************************************************)
 (** Pretty printings                                                        **)