From 897373ab09685b29cbfab8deb6c868ece21c5cc1 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 2 Oct 2009 09:21:39 +0000
Subject: [PATCH] Wrong context (again!)

---
 helm/software/components/ng_refiner/nCicRefiner.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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
-- 
2.39.2