metasenv,subst,item1::context
) (metasenv,subst,tys) sx_context_ty_rev sx_context_te_rev
with Invalid_argument "List.fold_left2" -> assert false in
+ 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
let con_sort= NCicTypeChecker.typeof ~subst ~metasenv context te in
(match
NCicReduction.whd ~subst context con_sort,