From 45bd81089d51747d96980020dab7ef34a7f79168 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 3 Oct 2008 11:01:02 +0000 Subject: [PATCH] the iterator was wrongly processing the application --- helm/software/components/ng_kernel/nCicUntrusted.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml index 655c8f17a..167fd47c9 100644 --- a/helm/software/components/ng_kernel/nCicUntrusted.ml +++ b/helm/software/components/ng_kernel/nCicUntrusted.ml @@ -22,14 +22,15 @@ let map_term_fold_a g k f a = function | C.Rel _ as t -> a,t | C.Appl [] | C.Appl [_] -> assert false | C.Appl l as orig -> - let a,l = + 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,[]) + List.fold_right + (fun t (a,l) -> let a,t = f k a t in a, t :: l) + l (a,[]) in - a, (match l with + a, if l1 == l then orig else (match l1 with | C.Appl l :: tl -> C.Appl (l@tl) - | l1 when l == l1 -> orig - | l1 -> C.Appl l1) + | _ -> C.Appl l1) | C.Prod (n,s,t) as orig -> let a,s1 = f k a s in let a,t1 = f (g (n,C.Decl s) k) a t in a, if t1 == t && s1 == s then orig else C.Prod (n,s1,t1) -- 2.39.2