From: Stefano Zacchiroli 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 **)