From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 21 Oct 2009 09:12:01 +0000 (+0000)
Subject: preserve sharing if map_term_fold_a
X-Git-Tag: make_still_working~3272
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ab72456f3d53035e6942f1cafa225d6759acf655;p=helm.git

preserve sharing if map_term_fold_a
---

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)
 ;;