From 150b18acd3964ff3356d0c11e1143bef5616ddc3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 4 Apr 2008 13:06:21 +0000 Subject: [PATCH] iterator map was mapping Lambdas to Prods!!! --- helm/software/components/ng_kernel/nCicUtils.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/ng_kernel/nCicUtils.ml b/helm/software/components/ng_kernel/nCicUtils.ml index 707ea93b6..1d43c2cbc 100644 --- a/helm/software/components/ng_kernel/nCicUtils.ml +++ b/helm/software/components/ng_kernel/nCicUtils.ml @@ -79,7 +79,7 @@ let map g k f = function if t1 == t && s1 == s then orig else NCic.Prod (n,s1,t1) | NCic.Lambda (n,s,t) as orig -> let s1 = f k s in let t1 = f (g (n,NCic.Decl s) k) t in - if t1 == t && s1 == s then orig else NCic.Prod (n,s1,t1) + if t1 == t && s1 == s then orig else NCic.Lambda (n,s1,t1) | NCic.LetIn (n,ty,t,b) as orig -> let ty1 = f k ty in let t1 = f k t in let b1 = f (g (n,NCic.Def (t,ty)) k) b in -- 2.39.2