]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_kernel/nCicUtils.ml
added # to comment
[helm.git] / 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