let ps, sort_disp = H.get_ind_parameters c arg in
let lps, rps = HEL.split_nth lpsno ps in
let rpsno = List.length rps in
+ if rpsno = 0 && sort_disp = 0 then
+(* FG: the transformation is not possible, we fall back into the plain case *)
+ opt_mutcase_plain g st es c uri tyno outty arg cases
+ else
let predicate = clear_absts rpsno (1 - sort_disp) outty in
let is_recursive t =
I.S.mem tyno (I.get_mutinds_of_uri uri t)