+let delift ~unify metasenv subst context n l t =
+ let is_in_scope_meta subst = function
+ | NCic.Meta (i,_) ->
+ (try
+ let tag, _, _, _ = NCicUtils.lookup_subst i subst in
+ tag = Some in_scope_tag
+ with NCicUtils.Subst_not_found _ -> false)
+ | _ -> false
+ in
+ let contains_in_scope subst t =
+ let rec aux _ () = function
+ | NCic.Meta _ as t ->
+ if is_in_scope_meta subst t then raise Found
+ else ()
+ | t ->
+ if is_in_scope_meta subst t then raise Found
+ else NCicUtils.fold (fun _ () -> ()) () aux () t
+ in
+ try aux () () t; false with Found -> true
+ in
+ let unify_list ~alpha in_scope =
+ match l with
+ | _, NCic.Irl _ -> fun _ _ _ _ _ -> None
+ | shift, NCic.Ctx l -> fun metasenv subst context k t ->
+ if flexible_arg subst t || contains_in_scope subst t then None else
+ let lb = List.map (fun t -> t, flexible_arg subst t) l in
+ HExtlib.list_findopt
+ (fun (li,flexible) i ->
+ if flexible || i < in_scope then None else
+ let li = NCicSubstitution.lift (k+shift) li in
+ if alpha then
+ if NCicReduction.alpha_eq metasenv subst context li t then
+ Some ((metasenv,subst), NCic.Rel (i+1+k))
+ else
+ None
+ else
+ match unify metasenv subst context li t with
+ | Some (metasenv,subst) ->
+ Some ((metasenv, subst), NCic.Rel (i+1+k))
+ | None -> None)
+ lb
+ in
+ let rec aux (context,k,in_scope) (metasenv, subst as ms) t =
+ match unify_list ~alpha:true in_scope metasenv subst context k t with
+ | Some x -> x
+ | None ->
+ try
+ match t with