From 6e2d3b0cabf805137a08f969840da05f8aba0adb Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 23 Apr 2008 08:17:26 +0000 Subject: [PATCH] Avoid other comparisons on universes using =. --- helm/software/components/cic/cicUniv.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml index 25f70bc0f..8570c0c15 100644 --- a/helm/software/components/cic/cicUniv.ml +++ b/helm/software/components/cic/cicUniv.ml @@ -648,11 +648,11 @@ let rec clean_ugraph m already_contained f = let e_l = MAL.fold (fun k v l -> if v = empty_entry && not(f k) then begin - k::l end else l) m'' [] + SOF.add k l end else l) m'' SOF.empty in - if e_l != [] then + if not (SOF.is_empty e_l) then clean_ugraph - m'' already_contained (fun u -> (f u) && not (List.mem u e_l)) + m'' already_contained (fun u -> (f u) && not (SOF.mem u e_l)) else MAL.fold (fun k v x -> if v <> empty_entry then MAL.add k v x else x) @@ -661,7 +661,8 @@ let rec clean_ugraph m already_contained f = let clean_ugraph (m,a,o) l = assert(not o); - let m, a = clean_ugraph m a (fun u -> List.mem u l) in + let l = List.fold_right SOF.add l SOF.empty in + let m, a = clean_ugraph m a (fun u -> SOF.mem u l) in m, a, o let assigner_of = -- 2.39.2