From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 4 Apr 2008 13:06:21 +0000 (+0000)
Subject: iterator map was mapping Lambdas to Prods!!!
X-Git-Tag: make_still_working~5451
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=150b18acd3964ff3356d0c11e1143bef5616ddc3;p=helm.git

iterator map was mapping Lambdas to Prods!!!
---

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