]> matita.cs.unibo.it Git - helm.git/commitdiff
iterator map was mapping Lambdas to Prods!!!
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 4 Apr 2008 13:06:21 +0000 (13:06 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 4 Apr 2008 13:06:21 +0000 (13:06 +0000)
helm/software/components/ng_kernel/nCicUtils.ml

index 707ea93b6f4a501c06d7d1535c99611751e1cfb1..1d43c2cbc3a69e18e18916a354f5ff9040859cd3 100644 (file)
@@ -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