X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=7395aa7ac7cd7679ea69f4f09ce62e4a97e3a092;hb=bb7f9a362891d4377011783016b74f0b0b2a5974;hp=5669b1abcd9bd4d500e220ae4c1d462fc067961f;hpb=86dbca4f0bfda375bdf036ec5ce3bf44678415f2;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 5669b1abc..7395aa7ac 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -135,10 +135,9 @@ let is_locked n subst =
    with NCicUtils.Subst_not_found _ -> false
 ;;
 
-let rec mk_irl =
- function
-    0 -> []
-  | n -> NCic.Rel n :: mk_irl (n-1)
+let rec mk_irl stop base =
+  if base > stop then []
+  else (NCic.Rel base) :: mk_irl stop (base+1) 
 ;;
 
 (* the argument must be a term in whd *)
@@ -168,15 +167,16 @@ let rec lambda_intros rdb metasenv subst context t args =
        metasenv, subst, bo
    | (arg,ty)::tail ->
        pp(lazy("arg{ " ^ 
-         NCicPp.ppterm ~metasenv ~subst ~context:context_of_args arg ^  ":" ^
+         NCicPp.ppterm ~metasenv ~subst ~context:context_of_args arg ^  " : " ^
          NCicPp.ppterm ~metasenv ~subst ~context:context_of_args ty));
        let metasenv, subst, telescopic_ty = 
          if processed_args = [] then metasenv, subst, ty else
          let _ = pp(lazy("delift")) in
-         delift_type_wrt_terms rdb metasenv subst context_of_args ty 
-           (List.rev processed_args)
+         delift_type_wrt_terms rdb metasenv subst context 
+           (NCicSubstitution.lift n ty)
+           (List.map (NCicSubstitution.lift n) (List.rev processed_args))
        in
-       pp(lazy("arg}"));
+       pp(lazy("arg} "^NCicPp.ppterm ~metasenv ~subst ~context telescopic_ty));
        let name = "HBeta"^string_of_int n in
        let metasenv, subst, bo =
         mk_lambda metasenv subst ((name,NCic.Decl telescopic_ty)::context) (n+1)
@@ -743,6 +743,7 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
  (*D*)  in outside true; rc with exn -> outside false; raise exn 
 
 and delift_type_wrt_terms rdb metasenv subst context t args =
+  let lc = List.rev args @ mk_irl (List.length context) (List.length args+1) in
   let (metasenv, subst), t =
    try
     NCicMetaSubst.delift 
@@ -753,8 +754,7 @@ and delift_type_wrt_terms rdb metasenv subst context t args =
            with UnificationFailure _ | Uncertain _ -> None
          in
          indent := ind; res)
-      metasenv subst context 0 (0,NCic.Ctx (args @ 
-        List.rev (mk_irl (List.length context)))) t
+      metasenv subst context 0 (0,NCic.Ctx lc) t
    with NCicMetaSubst.MetaSubstFailure _ -> (metasenv, subst), t
   in
    metasenv, subst, t