+ let ty2,_ =
+ CicTypeChecker.type_of_aux' metasenv context t2 CicUniv.oblivion_ugraph
+ in
+ let saturated_ty2, menv_for_saturated_ty2, args_t2 =
+ let maxm = CicMkImplicit.new_meta metasenv [] in
+ let ty2, menv, args, _ =
+ TermUtil.saturate_term ~delta:false maxm metasenv context ty2 0 in
+ ty2, menv, args
+ in
+ let saturations_t2 =
+ let rec aux n = function
+ | Cic.Meta (i,_)::tl ->
+ let _,c,ty = CicUtil.lookup_meta i menv_for_saturated_ty2 in
+ if fst (CicReduction.are_convertible c ty (Cic.Sort Cic.Prop)
+ CicUniv.oblivion_ugraph)
+ then n else aux (n+1) tl
+ | _::tl -> aux (n+1) tl
+ | [] -> n+1
+ in
+ List.length args_t2 - aux 0 args_t2 +1
+ in
+ debug_print (lazy("saturated_ty2: "^CicMetaSubst.ppterm_in_context
+ [] ~metasenv:menv_for_saturated_ty2 saturated_ty2 context ^
+ " saturations_t2:" ^ string_of_int saturations_t2));
+ (* unifies t with saturated_ty2 and gives back a fresh meta of type t *)
+ let unif menv t =
+ let m, menv2 =
+ let n = CicMkImplicit.new_meta menv [] in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context
+ in
+ Cic.Meta (n,irl), ((n,context,t)::menv)
+ in
+ try
+ let _ =
+ CicUnification.fo_unif menv context t saturated_ty2
+ CicUniv.oblivion_ugraph
+ in
+ true, menv2, m
+ with
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ -> false, menv2, m
+ in
+ (* check which "positions" in the input arrow unifies with saturated_ty2 *)
+ let rec positions menv cur saturations = function
+ | Cic.Prod (n,s,t) ->
+ let b, newmenv, sb = unif menv s in
+ if b then
+ (saturations - cur - 1) ::
+ (positions newmenv (cur + 1) saturations
+ (CicSubstitution.subst sb t))
+ else
+ positions newmenv (cur + 1) saturations (CicSubstitution.subst sb t)
+ | _ -> []
+ in
+ (* position is a list of arities, that is if t1 : a -> b -> c and saturations
+ * is 0 then the computed term will be (t1 ? t2) of type a -> c if saturations
+ * is 1 then (t1 t2 ?) of type b -> c *)
+ let rec generate positions menv acc =
+ match positions with
+ | [] -> acc, menv
+ | saturations_t1::tl ->