+(* BEGIN FIX OUT TYPE *)
+ let lpsno, psno = get_ind_type_psnos u m in
+ let rpsno = psno - lpsno in
+ let named, frpsno, wc, wb = split_absts true 0 [] w' in
+ let w' =
+(* No fixing needed *)
+ if frpsno = succ rpsno then w' else
+(* Fixing needed, no right parametes *)
+ if frpsno = rpsno && rpsno = 0 then
+ let vty, _ = TC.type_of_aux' [] st.c v' Un.default_ugraph in
+ if !debug then begin
+ out "VTY: "; Ut.pp_term out [] st.c vty; out "\n"
+ end;
+ C.Lambda (C.Anonymous, vty, S.lift 1 wb)
+ else
+(* Fixing needed, some right parametes *)
+ if frpsno = rpsno && named then
+ let vty, _ = TC.type_of_aux' [] st.c v' Un.default_ugraph in
+ if !debug then begin
+ out "VTY: "; Ut.pp_term out [] st.c vty; out "\n"
+ end;
+ let vty, wb = S.lift rpsno vty, S.lift 1 wb in
+ let vty = match vty with
+ | C.Appl (C.MutInd (fu, fm, _) as hd :: args)
+ when UM.eq fu u && fm = m && List.length args = psno ->
+ let largs, _ = X.split_nth lpsno args in
+ C.Appl (hd :: largs @ Ut.mk_rels rpsno 0)
+ | _ ->
+ assert false
+ in
+ close false wc (C.Lambda (C.Anonymous, vty, wb))
+(* This case should not happen *)
+ else assert false
+ in
+(* END FIX OUT TYPE *)
+ if UM.eq u u' && w' == w && v' == v && vs' == vs then t else
+ C.MutCase (u', m, sh w w', sh v v', sh vs vs')