+ let metasenv, subst =
+ let rec aux context (metasenv,subst) = function
+ | NCic.Meta _ -> metasenv, subst
+ | NCic.Implicit _ -> metasenv, subst
+ | NCic.Appl (NCic.Rel i :: args) as t
+ when i > List.length context - len ->
+ let lefts, _ = HExtlib.split_nth leftno args in
+ let ctxlen = List.length context in
+ let (metasenv, subst), _ =
+ List.fold_left
+ (fun ((metasenv, subst),l) arg ->
+ NCicUnification.unify rdb
+ ~test_eq_only:true metasenv subst context arg
+ (NCic.Rel (ctxlen - len - l)), l+1
+ )
+ ((metasenv, subst), 0) lefts
+ in
+ metasenv, subst
+ | t -> NCicUtils.fold (fun e c -> e::c) context aux
+ (metasenv,subst) t
+ in
+ aux context (metasenv,subst) te
+ in