uses Map.equal to compare universes

diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml
index e79a2a9d9eae1034188ac38a7eaec416c528062a..5616cb675daf9770bb84ad7edeee6b3fde82d4b6 100644 (file)
--- 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                                                        **)