let eliminator = H.get_default_eliminator c uri tyno outty in
let lpsno, (_, _, _, constructors) = H.get_ind_type uri tyno in
let ps, sort_disp = H.get_ind_parameters c arg in
let eliminator = H.get_default_eliminator c uri tyno outty in
let lpsno, (_, _, _, constructors) = H.get_ind_type uri tyno in
let ps, sort_disp = H.get_ind_parameters c arg in