opt_mutcase_plain g st es c uri tyno outty arg cases
else
let predicate = clear_absts rpsno (1 - sort_disp) outty in
+ if H.occurs c ~what:(C.Rel 0) ~where:predicate 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 is_recursive t =
I.S.mem tyno (I.get_mutinds_of_uri uri t)
in