From ab72456f3d53035e6942f1cafa225d6759acf655 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 21 Oct 2009 09:12:01 +0000 Subject: [PATCH] preserve sharing if map_term_fold_a --- helm/software/components/ng_kernel/nCicUntrusted.ml | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml index 771568018..b48db58ec 100644 --- a/helm/software/components/ng_kernel/nCicUntrusted.ml +++ b/helm/software/components/ng_kernel/nCicUntrusted.ml @@ -25,12 +25,7 @@ let map_term_fold_a g k f a = function let fire_beta, upto = match l with C.Meta _ :: _ -> true, List.length l - 1 | _ -> false, 0 in - let a,l1 = - (* sharing fold? *) - List.fold_right - (fun t (a,l) -> let a,t = f k a t in a, t :: l) - l (a,[]) - in + let a,l1 = HExtlib.sharing_map_acc (f k) a l in a, if l1 == l then orig else let t = match l1 with @@ -51,10 +46,7 @@ let map_term_fold_a g k f a = function a, if ty1 == ty && t1 == t && b1 == b then orig else C.LetIn (n,ty1,t1,b1) | C.Match (r,oty,t,pl) as orig -> let a,oty1 = f k a oty in let a,t1 = f k a t in - let a,pl1 = - (* sharing fold? *) - List.fold_right (fun t (a,l) -> let a,t = f k a t in a,t::l) pl (a,[]) - in + let a,pl1 = HExtlib.sharing_map_acc (f k) a pl in a, if oty1 == oty && t1 == t && pl1 == pl then orig else C.Match(r,oty1,t1,pl1) ;; -- 2.39.2