- delift_type_wrt_term fixed in many ways

[helm.git] / helm / software / components / ng_refiner / nCicUnification.ml

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 5669b1abcd9bd4d500e220ae4c1d462fc067961f..7395aa7ac7cd7679ea69f4f09ce62e4a97e3a092 100644 (file)
--- 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