From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 2 Oct 2009 09:21:39 +0000 (+0000)
Subject: Wrong context (again!)
X-Git-Tag: make_still_working~3399
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=897373ab09685b29cbfab8deb6c868ece21c5cc1;p=helm.git

Wrong context (again!)
---

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index f46487aab..e2aabb31c 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -242,7 +242,8 @@ let rec typeof rdb
          | Some x -> 
              let m, s, x = 
                NCicUnification.delift_type_wrt_terms 
-               rdb metasenv subst context x [t]
+                rdb metasenv subst context1 (NCicSubstitution.lift 1 x)
+                [NCicSubstitution.lift 1 t]
              in
                m, s, Some x
        in