- let ty2, menv, _, _ = TermUtil.saturate_term maxm metasenv context ty2 0 in
- ty2, menv
+ 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