X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicUtils.ml;h=1d43c2cbc3a69e18e18916a354f5ff9040859cd3;hb=725115d4f97b92666c4241f88b4f337f9d07a79f;hp=707ea93b6f4a501c06d7d1535c99611751e1cfb1;hpb=5ba3b166fff4398b031774b52bd7c1ae1e5be09b;p=helm.git

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